diff --git a/include/generic_datatype.h b/include/generic_datatype.h index 9700eaeb6..637cc859f 100644 --- a/include/generic_datatype.h +++ b/include/generic_datatype.h @@ -25,11 +25,16 @@ class GenericDatatypeDecl : public AbsDatatypeDecl public: GenericDatatypeDecl(const std::string name); virtual ~GenericDatatypeDecl(){}; - std::string get_name(); + std::string get_name() const; + int get_param_count() const; + std::vector get_param_sorts(); + void register_param_sort(std::string param_name); protected: friend class GenericSolver; std::string dt_name; + int param_count; + std::vector param_sorts; }; class GenericDatatypeConstructorDecl : public AbsDatatypeConstructorDecl @@ -46,10 +51,13 @@ class GenericDatatypeConstructorDecl : public AbsDatatypeConstructorDecl int get_selector_count() const; bool compare(const DatatypeConstructorDecl & d) const override; std::string get_dt_name() const; + void add_selector_param(const std::string & name, int param_num); protected: std::vector selector_vector; std::string cons_name; + bool contains_param; + DatatypeDecl dt_decl; // Setter for the dt_decl member. Only to be used when a constructor // is added to a datatype. datatype_decl: The DatatypeDecl of the datatype. @@ -85,6 +93,7 @@ class GenericDatatype : public AbsDatatype protected: DatatypeDecl dt_decl; + std::vector cons_decl_vector; friend class GenericSolver; diff --git a/include/generic_solver.h b/include/generic_solver.h index ce8cd6532..aa832c305 100644 --- a/include/generic_solver.h +++ b/include/generic_solver.h @@ -50,7 +50,9 @@ class GenericSolver : public AbsSmtSolver Sort make_sort(const Sort & sort_con, const SortVec & sorts) const override; // Mutually recursive datatypes are currently not supported. Sort make_sort(const DatatypeDecl & d) const override; + DatatypeDecl make_datatype_decl(const std::string & s) override; + DatatypeConstructorDecl make_datatype_constructor_decl( const std::string s) override; void add_constructor(DatatypeDecl & dt, @@ -60,11 +62,16 @@ class GenericSolver : public AbsSmtSolver const Sort & s) const override; void add_selector_self(DatatypeConstructorDecl & dt, const std::string & name) const override; + Sort get_unresolved_sort(DatatypeDecl dt_decl); + Term get_constructor(const Sort & s, std::string name) const override; Term get_tester(const Sort & s, std::string name) const override; Term get_selector(const Sort & s, std::string con, std::string name) const override; + SortVec make_datatype_sorts( + const std::vector & decls, + const UnorderedSortSet & uninterp_sorts) const override; /***************************************************************/ /* methods from AbsSmtSolver that are implemented */ @@ -266,6 +273,7 @@ class GenericSolver : public AbsSmtSolver std::unique_ptr< std::unordered_map, std::string>> datatype_name_map; + std::unique_ptr> par_map; }; } // namespace smt diff --git a/include/generic_sort.h b/include/generic_sort.h index 256a28f82..ae0dea374 100644 --- a/include/generic_sort.h +++ b/include/generic_sort.h @@ -26,6 +26,7 @@ namespace smt { class GenericDatatye; + /* Helper functions for creating generic sorts */ Sort make_uninterpreted_generic_sort(std::string name, uint64_t arity); Sort make_uninterpreted_generic_sort(Sort sort_cons, const SortVec& sorts); @@ -37,6 +38,9 @@ Sort make_generic_sort(SortKind sk, Sort sort1, Sort sort2, Sort sort3); Sort make_generic_sort(SortKind sk, SortVec sorts); Sort make_generic_sort(Datatype dt); Sort make_generic_sort(SortKind sk, std::string cons_name, Sort dt); +Sort make_generic_param_sort(std::string param_name); +Sort make_generic_datatype_sort(Datatype dt); +Sort make_generic_unresolved_sort(DatatypeDecl dt); /* smtlib representation of sort kinds */ std::string to_smtlib(SortKind); @@ -232,4 +236,32 @@ class DatatypeComponentSort : public GenericSort Sort selector_sort; }; +class ParamSort : public GenericSort +{ + public: + ParamSort(std::string param_name); + ~ParamSort(){}; + std::string get_uninterpreted_name() const override; + std::string compute_string() const override; + + protected: + std::string name; +}; + +class UnresolvedSort : public GenericSort +{ + public: + UnresolvedSort(DatatypeDecl dt_decl); + ~UnresolvedSort(){}; + std::string compute_string() const override; + std::string to_string() const override; + DatatypeDecl get_datatype_decl(); + std::vector get_params(); + void insert_param(std::string new_param); + + protected: + DatatypeDecl datatype_decl; + std::vector params_vector; +}; + } // namespace smt diff --git a/include/solver.h b/include/solver.h index 14b35cb50..ceb01b056 100644 --- a/include/solver.h +++ b/include/solver.h @@ -239,15 +239,15 @@ class AbsSmtSolver * If no symbol of that name has been declared, throws * IncorrectUsageException * - * Allows a user to look up a symbol by name. This can be very useful for term - * translation, since we can look up symbols instead of keeping track of the - * mapping via externally populated caches (in the case where the target + * Allows a user to look up a symbol by name. This can be very useful for + * term translation, since we can look up symbols instead of keeping track of + * the mapping via externally populated caches (in the case where the target * solver has already been used). * - * Note, solver backend deals with the implementation. The main motivation for - * this is that each backend solver has to own the symbol table. If the symbol - * table were stored in AbsSmtSolver then it would get destructed after the - * backend solver which has bad refcounting implications for many solvers. + * Note, solver backend deals with the implementation. The main motivation + * for this is that each backend solver has to own the symbol table. If the + * symbol table were stored in AbsSmtSolver then it would get destructed after + * the backend solver which has bad refcounting implications for many solvers. * * @param name the name of the symbol to look up * @return the Term representation of the corresponding symbol diff --git a/include/sort.h b/include/sort.h index f291bae12..18da044ac 100644 --- a/include/sort.h +++ b/include/sort.h @@ -47,6 +47,8 @@ enum SortKind CONSTRUCTOR, SELECTOR, TESTER, + PARAM, + UNRESOLVED, /** IMPORTANT: This must stay at the bottom. It's only use is for sizing the kind2str array diff --git a/src/generic_datatype.cpp b/src/generic_datatype.cpp index c7dd1dd9f..dea89c276 100644 --- a/src/generic_datatype.cpp +++ b/src/generic_datatype.cpp @@ -11,15 +11,37 @@ using namespace std; namespace smt { -GenericDatatypeDecl::GenericDatatypeDecl(const std::string name) : dt_name(name) +GenericDatatypeDecl::GenericDatatypeDecl(const std::string name) + : dt_name(name), param_count(0) { } -std::string GenericDatatypeDecl::get_name() { return dt_name; } +std::string GenericDatatypeDecl::get_name() const { return dt_name; } + +int GenericDatatypeDecl::get_param_count() const { return param_count; } + +std::vector GenericDatatypeDecl::get_param_sorts() { return param_sorts; } + +void GenericDatatypeDecl::register_param_sort(std::string param_name) +{ + for (unsigned int i = 0; i < param_count; ++i) + { + // Checks if the selector has already been added + if (param_sorts[i]->to_string() == param_name) + { + // throw "Can't add selector. It already exists in this + // datatype!"; + return; + } + } + Sort new_param = make_generic_param_sort(param_name); + param_sorts.push_back(new_param); + param_count += 1; +} GenericDatatypeConstructorDecl::GenericDatatypeConstructorDecl( const std::string & name) - : cons_name(name) + : cons_name(name), contains_param(false) { } @@ -87,6 +109,21 @@ void GenericDatatype::add_constructor( } shared_ptr gdt_cons = static_pointer_cast(dt_cons_decl); + + if (gdt_cons->contains_param == true) + { + for (int i = 0; i < gdt_cons->get_selector_count(); ++i) + { + if (gdt_cons->get_selector_vector()[i].sort->get_sort_kind() + == SortKind::PARAM) + { + static_pointer_cast(dt_decl)->register_param_sort( + static_pointer_cast( + gdt_cons->get_selector_vector()[i].sort) + ->to_string()); + } + } + } // Links the constructor to the datatype_decl of the datatype gdt_cons->update_stored_dt(dt_decl); // Links the datatype to the new constructor diff --git a/src/generic_solver.cpp b/src/generic_solver.cpp index 9ed6f70ea..13a2f9ecc 100644 --- a/src/generic_solver.cpp +++ b/src/generic_solver.cpp @@ -82,7 +82,8 @@ GenericSolver::GenericSolver(string path, name_datatype_map( new unordered_map>()), datatype_name_map( - new unordered_map, string>()) + new unordered_map, string>()), + par_map(new unordered_map()) { // Buffer sizes over 256 caused issues in tests. // Until this is investigated, we support a conservative @@ -111,6 +112,7 @@ GenericSolver::GenericSolver(string path, for (int i=0; i < read_buf_size; i++) { read_buf[i]=0; } + *par_map = { { 0, "T" }, { 1, "F" }, { 2, "Q" } }; // start the process with the solver binary start_solver(); } @@ -487,10 +489,29 @@ Sort GenericSolver::make_sort(const SortKind sk, Sort GenericSolver::make_sort(SortKind sk, const SortVec & sorts) const { - // create the sort - Sort sort = make_generic_sort(sk, sorts); - // compute the name - string name = sort->to_string(); + string name; + Sort sort; + if (sk == SortKind::PARAM) + { + name = sorts[0]->to_string(); + sort = make_generic_param_sort(name); + } + else if (sk == SortKind::UNRESOLVED && sorts.size() == 1) + { + cout << "in make sort" << endl; + shared_ptr dt_sort = + static_pointer_cast(sorts[0]); + name = dt_sort->to_string(); + sort = make_generic_unresolved_sort(dt_sort->get_datatype_decl()); + return sort; + } + else + { + // create the sort + sort = make_generic_sort(sk, sorts); + // compute the name + name = sort->to_string(); + } // note that nothing needs to be communicated to the solver, // as in this case the sort is built in, or can used @@ -525,8 +546,21 @@ Sort GenericSolver::make_sort(const DatatypeDecl & d) const std::string to_solver = "(" + DECLARE_DATATYPE_STR + " (("; to_solver += dt_decl_name; - to_solver += " 0)) (\n"; + to_solver += " "; + to_solver += std::to_string(gdt_decl->get_param_count()); + to_solver += ")) (\n"; to_solver += "("; + if (gdt_decl->get_param_count()) + { + to_solver += "par ("; + for (int g = 0; g < gdt_decl->get_param_count(); ++g) + { + to_solver += gdt_decl->get_param_sorts()[g]->to_string(); + to_solver += " "; + } + to_solver += ")"; + to_solver += " ("; + } // build string for each constructor for (unsigned long i = 0; i < curr_dt->get_cons_vector().size(); ++i) { @@ -548,21 +582,42 @@ Sort GenericSolver::make_sort(const DatatypeDecl & d) const curr_dt_cons_decl) ->get_selector_vector()[f] .name; - to_solver += " " - + (static_pointer_cast( - curr_dt_cons_decl) - ->get_selector_vector()[f] - .sort) - ->to_string() - + " )"; + auto gdtc_cast = static_pointer_cast( + curr_dt_cons_decl); + if ((gdtc_cast->get_selector_vector()[f].sort)->to_string() + == gdt_decl->get_name() + && gdtc_cast->contains_param) + { + to_solver += " ("; + to_solver += + (gdtc_cast->get_selector_vector()[f].sort)->to_string() + " "; + for (int t = 0; t < gdt_decl->get_param_count(); ++t) + { + to_solver += gdt_decl->get_param_sorts()[t]->to_string(); + to_solver += " "; + } + to_solver += "))"; + } + else + { + to_solver += " " + + (static_pointer_cast( + curr_dt_cons_decl) + ->get_selector_vector()[f] + .sort) + ->to_string() + + " )"; + } } to_solver += ")"; } + to_solver += gdt_decl->get_param_count() ? ")" : ""; to_solver += ")\n))"; assert(name_sort_map->find(dt_decl_name) == name_sort_map->end()); (*name_sort_map)[dt_decl_name] = dt_sort; (*sort_name_map)[dt_sort] = dt_decl_name; + cout << to_solver << endl; run_command(to_solver); return dt_sort; @@ -576,13 +631,15 @@ Sort GenericSolver::make_sort(const DatatypeDecl & d) const DatatypeDecl GenericSolver::make_datatype_decl(const std::string & s) { - DatatypeDecl new_dt_decl = make_shared(s); + shared_ptr new_dt_decl = + make_shared(s); shared_ptr new_dt = shared_ptr(new GenericDatatype(new_dt_decl)); (*name_datatype_map)[s] = new_dt; (*datatype_name_map)[new_dt] = s; return new_dt_decl; } + DatatypeConstructorDecl GenericSolver::make_datatype_constructor_decl( const std::string s) { @@ -605,11 +662,32 @@ void GenericSolver::add_selector(DatatypeConstructorDecl & dt, const std::string { shared_ptr newSelector = make_shared(); - newSelector->name = name; - newSelector->sort = s; - newSelector->finalized = true; shared_ptr gdtc = static_pointer_cast(dt); + + newSelector->name = name; + if (s->get_sort_kind() == SortKind::PARAM) + { + newSelector->sort = s; + gdtc->contains_param = true; + } + else if (s->get_sort_kind() == UNRESOLVED) + { + auto gdt_decl = static_pointer_cast( + static_pointer_cast(dt)->dt_decl); + auto dt_sort = static_pointer_cast(s); + for (int i = 0; i < dt_sort->get_params().size(); i++) + { + gdt_decl->register_param_sort(dt_sort->get_params()[i]); + } + newSelector->sort = s; + newSelector->finalized = true; + } + else + { + newSelector->sort = s; + } + newSelector->finalized = true; gdtc->add_new_selector(*newSelector); } @@ -633,6 +711,19 @@ void GenericSolver::add_selector_self(DatatypeConstructorDecl & dt, const std::s gdt_cons->add_new_selector(*newSelector); } +Sort GenericSolver::get_unresolved_sort(DatatypeDecl dt_decl) +{ + shared_ptr gdt_decl = + static_pointer_cast(dt_decl); + string dt_decl_name = gdt_decl->get_name(); + assert(name_datatype_map->find(dt_decl_name) != name_datatype_map->end()); + shared_ptr curr_dt = (*name_datatype_map)[dt_decl_name]; + Sort dt_sort = make_generic_datatype_sort(curr_dt); + (*name_sort_map)[dt_decl_name] = dt_sort; + (*sort_name_map)[dt_sort] = dt_decl_name; + return dt_sort; +} + Term GenericSolver::get_constructor(const Sort & s, std::string name) const { shared_ptr dt = @@ -727,6 +818,105 @@ Term GenericSolver::get_selector(const Sort & s, std::string con, std::string na return (*name_term_map)[name]; } +SortVec GenericSolver::make_datatype_sorts( + const std::vector & decls, + const UnorderedSortSet & uninterp_sorts) const +{ + assert(decls.size()); + assert(uninterp_sorts.size()); + std::vector rec_sorts; + std::string to_solver = "(" + DECLARE_DATATYPE_STR + " ("; + for (auto decl : decls) + { + to_solver += + " (" + static_pointer_cast(decl)->get_name() + " " + + std::to_string( + static_pointer_cast(decl)->get_param_count()) + + ")"; + } + to_solver += ") ("; + shared_ptr curr_decl; + shared_ptr curr_dt; + for (auto decl : decls) + { + curr_decl = static_pointer_cast(decl); + curr_dt = (*name_datatype_map)[curr_decl->get_name()]; + to_solver += "\n; " + curr_decl->get_name() + "\n"; + if (curr_decl->get_param_count()) + { + to_solver += "(par ("; + for (int g = 0; g < curr_decl->get_param_count(); ++g) + { + to_solver += curr_decl->get_param_sorts()[g]->to_string(); + to_solver += " "; + } + to_solver += ")"; + } + to_solver += " ( "; + for (auto cons : curr_dt->get_cons_vector()) + { + to_solver += " (" + + static_pointer_cast(cons) + ->get_name(); + for (auto selector : + static_pointer_cast(cons) + ->get_selector_vector()) + { + to_solver += " ( " + selector.name + " "; + if (selector.sort->get_sort_kind() == UNRESOLVED) + { + if (static_pointer_cast(selector.sort) + ->get_params() + .size() + > 0) + { + to_solver += "(" + + static_pointer_cast(selector.sort) + ->to_string(); + for (auto param : static_pointer_cast(selector.sort) + ->get_params()) + { + to_solver += " " + param; + } + to_solver += ")"; + } + else + { + to_solver += + static_pointer_cast(selector.sort)->to_string(); + } + } + else + { + to_solver += selector.sort->to_string(); + } + to_solver += ")"; + } + to_solver += ")"; + } + to_solver += "))"; + } + to_solver += " ))"; + cout << to_solver << end; + run_command(to_solver); + for (auto decl : decls) + { + Sort rec_sort = make_generic_datatype_sort( + (*name_datatype_map)[static_pointer_cast(decl) + ->get_name()]); + assert(name_sort_map->find( + static_pointer_cast(decl)->get_name()) + == name_sort_map->end()); + (*name_sort_map)[static_pointer_cast(decl) + ->get_name()] = rec_sort; + (*sort_name_map)[rec_sort] = + static_pointer_cast(decl)->get_name(); + rec_sorts.push_back(rec_sort); + } + + return rec_sorts; +} + std::string GenericSolver::get_name(Term term) const { // the names of the terms are `t_i` with a running `i`. diff --git a/src/generic_sort.cpp b/src/generic_sort.cpp index 6efdae453..5864f5550 100644 --- a/src/generic_sort.cpp +++ b/src/generic_sort.cpp @@ -130,6 +130,19 @@ Sort make_generic_sort(SortKind sk, std::string cons_name, Sort dt) return make_shared(sk, cons_name, dt); } +Sort make_generic_param_sort(std::string param_name) +{ + return make_shared(param_name); +} +Sort make_generic_datatype_sort(Datatype dt) +{ + return make_shared(dt); +} +Sort make_generic_unresolved_sort(DatatypeDecl dt) +{ + return make_shared(dt); +} + // implementations GenericSort::GenericSort(SortKind sk) : sk(sk) {} @@ -197,6 +210,10 @@ string GenericSort::compute_string() const { { return get_uninterpreted_name(); } + else if (get_sort_kind() == SortKind::PARAM) + { + return get_uninterpreted_name(); + } else { assert(false); @@ -448,7 +465,6 @@ Sort DatatypeComponentSort::get_codomain_sort() const { return selector_sort; } - assert(sk == CONSTRUCTOR || sk == TESTER || sk == SELECTOR); } @@ -469,4 +485,33 @@ Datatype DatatypeComponentSort::get_datatype() const return dt_sort->get_datatype(); } +ParamSort::ParamSort(std::string param_name) + : name(param_name), GenericSort(SortKind::PARAM) +{ +} + +std::string ParamSort::compute_string() const { return name; } +std::string ParamSort::get_uninterpreted_name() const { return name; } + +UnresolvedSort::UnresolvedSort(DatatypeDecl dt_decl) + : datatype_decl(dt_decl), GenericSort(SortKind::UNRESOLVED) +{ +} + +std::string UnresolvedSort::compute_string() const +{ + return static_pointer_cast(datatype_decl)->get_name(); +} + +std::string UnresolvedSort::to_string() const { return compute_string(); } + +DatatypeDecl UnresolvedSort::get_datatype_decl() { return datatype_decl; } + +std::vector UnresolvedSort::get_params() { return params_vector; } + +void UnresolvedSort::insert_param(std::string new_param) +{ + params_vector.push_back(new_param); +} + } // namespace smt diff --git a/src/sort.cpp b/src/sort.cpp index 5bdd671cf..b063cc86f 100644 --- a/src/sort.cpp +++ b/src/sort.cpp @@ -32,7 +32,8 @@ const std::unordered_map sortkind2str( { FUNCTION, "Function" }, { UNINTERPRETED, "Uninterpreted" }, { UNINTERPRETED_CONS, "UninterpretedSortConstructor" }, - { DATATYPE, "Datatype" } }); + { DATATYPE, "Datatype" }, + { PARAM, "Parameterized" } }); std::string to_string(SortKind sk) { diff --git a/src/utils.cpp b/src/utils.cpp index f4e14d4c2..d0af5b5c0 100644 --- a/src/utils.cpp +++ b/src/utils.cpp @@ -250,9 +250,9 @@ void cnf_to_dimacs(Term cnf, std::ostringstream & y) smt::Op op = t->get_op(); assert(op.is_null() || op == smt::Or || op == smt::Not); - if(op.prim_op == smt::Or) + if (op.prim_op == smt::Or) { - for(auto u : t) + for (auto u : t) { before_or_elimination.push_back(u); } @@ -264,74 +264,74 @@ void cnf_to_dimacs(Term cnf, std::ostringstream & y) } } clauses.push_back(after_or_elimination); - } - - std::map ma; // This map will create a mapping from symbols to - // distinct contiguous integer values. - int ptr = 0; // pointer to store the next integer used in mapping - - // iterating within each clause and mapping every distinct symbol to a - // natural number - for (auto u : clauses) - { - for (auto uu : u) - { // Using literals from all the clauses to create the mapping - if (uu->is_value() && uu->to_string() == "false") - { // For an empty clause, which will just contain the term "false" - } - else if (uu->is_symbolic_const()) - { // A positive literal - if (ma.find(uu) == ma.end()) - { // Checking if symbol is absent in the mapping done till now - ptr++; - ma[uu] = ptr; - } - } - else - { // A negative literal - Term t = (*(uu->begin())); - if (ma.find(t) == ma.end()) - { - ptr++; - ma[t] = ptr; - } - } - } - } - //printing the output in DIMACS format - y << "p cnf "; - y << ptr; // number of distinct symbols - y << " "; - - int sz = clauses.size(); - - y << sz; // number of clauses - y << "\n"; - - // iterating within each clause and assigning the literal their mapped - // value(for a positive literal) or it's negative value(for a negative - // literal) - for (auto u : clauses) - { - for (auto uu : u) - { - if (uu->is_value() && uu->to_string() == "false") - { // For an empty clause - } - else if (uu->is_symbolic_const()) - { - y << (ma[uu]); // Positive number for a positive literal - y << " "; - } - else - { - Term t = (*(uu->begin())); - y << ((-(ma[t]))); // Negative number for a negative literal - y << " "; - } - } - y << 0; // Symbolizing end of line - y << "\n"; + } + + std::map ma; // This map will create a mapping from symbols to + // distinct contiguous integer values. + int ptr = 0; // pointer to store the next integer used in mapping + + // iterating within each clause and mapping every distinct symbol to a + // natural number + for (auto u : clauses) + { + for (auto uu : u) + { // Using literals from all the clauses to create the mapping + if (uu->is_value() && uu->to_string() == "false") + { // For an empty clause, which will just contain the term "false" + } + else if (uu->is_symbolic_const()) + { // A positive literal + if (ma.find(uu) == ma.end()) + { // Checking if symbol is absent in the mapping done till now + ptr++; + ma[uu] = ptr; + } + } + else + { // A negative literal + Term t = (*(uu->begin())); + if (ma.find(t) == ma.end()) + { + ptr++; + ma[t] = ptr; + } + } + } + } + // printing the output in DIMACS format + y << "p cnf "; + y << ptr; // number of distinct symbols + y << " "; + + int sz = clauses.size(); + + y << sz; // number of clauses + y << "\n"; + + // iterating within each clause and assigning the literal their mapped + // value(for a positive literal) or it's negative value(for a negative + // literal) + for (auto u : clauses) + { + for (auto uu : u) + { + if (uu->is_value() && uu->to_string() == "false") + { // For an empty clause + } + else if (uu->is_symbolic_const()) + { + y << (ma[uu]); // Positive number for a positive literal + y << " "; + } + else + { + Term t = (*(uu->begin())); + y << ((-(ma[t]))); // Negative number for a negative literal + y << " "; + } + } + y << 0; // Symbolizing end of line + y << "\n"; } } diff --git a/tests/test-dt.cpp b/tests/test-dt.cpp index d140da82b..5e907986b 100644 --- a/tests/test-dt.cpp +++ b/tests/test-dt.cpp @@ -184,6 +184,74 @@ TEST_P(DTTests, DatatypeDecl) EXPECT_THROW(listdt->get_num_selectors("kons"), InternalSolverException); } +TEST_P(DTTests, param_datatypes) +{ + // in future, we should have a better parameterization + // I can help with that, but for now this would work + SolverConfiguration sc = GetParam(); + if (sc.solver_enum != GENERIC_SOLVER) + { + return; + } + if (sc.is_logging_solver) + { + return; + } + + DatatypeDecl pair_decl = s->make_datatype_decl("Pair"); + DatatypeConstructorDecl pair_cons = s->make_datatype_constructor_decl("pair"); + s->add_selector( + pair_cons, "first", s->make_sort(PARAM, make_generic_param_sort("X"))); + s->add_selector( + pair_cons, "second", s->make_sort(PARAM, make_generic_param_sort("Y"))); + s->add_constructor(pair_decl, pair_cons); + Sort pairSort = s->make_sort(pair_decl); + + DatatypeDecl par_list = s->make_datatype_decl("List"); + DatatypeConstructorDecl par_nil = s->make_datatype_constructor_decl("nil"); + DatatypeConstructorDecl par_cons = s->make_datatype_constructor_decl("cons"); + s->add_selector( + par_cons, "car", s->make_sort(PARAM, make_generic_param_sort("T"))); + s->add_constructor(par_list, par_nil); + s->add_constructor(par_list, par_cons); + s->add_selector_self(par_cons, "cdr"); + Sort par_sort = s->make_sort(par_list); + + std::unordered_set unresTypes; + DatatypeDecl tree = s->make_datatype_decl("Tree"); + DatatypeDecl tree_list = s->make_datatype_decl("TreeList"); + DatatypeConstructorDecl empty_cons = + s->make_datatype_constructor_decl("empty"); + s->add_constructor(tree_list, empty_cons); + DatatypeConstructorDecl node_cons = s->make_datatype_constructor_decl("node"); + Sort tree_sort = s->make_sort(UNRESOLVED, make_generic_unresolved_sort(tree)); + Sort tree_list_sort_X = + s->make_sort(UNRESOLVED, make_generic_unresolved_sort(tree_list)); + Sort tree_list_sort_Y = + s->make_sort(UNRESOLVED, make_generic_unresolved_sort(tree_list)); + static_pointer_cast(tree_sort)->insert_param("Y"); + static_pointer_cast(tree_list_sort_X)->insert_param("X"); + static_pointer_cast(tree_list_sort_Y)->insert_param("Y"); + + unresTypes.insert(tree_sort); + unresTypes.insert(tree_list_sort_Y); + s->add_selector( + node_cons, "value", s->make_sort(PARAM, make_generic_param_sort("X"))); + s->add_constructor(tree, node_cons); + s->add_selector(node_cons, "children", tree_list_sort_X); + DatatypeConstructorDecl insert_cons = + s->make_datatype_constructor_decl("insert"); + + s->add_constructor(tree_list, insert_cons); + s->add_selector(insert_cons, "head", tree_sort); + s->add_selector(insert_cons, "tail", tree_list_sort_Y); + std::vector dtdecls; + dtdecls.push_back(tree); + dtdecls.push_back(tree_list); + std::vector dtsorts; + dtsorts = s->make_datatype_sorts(dtdecls, unresTypes); +} + INSTANTIATE_TEST_SUITE_P(ParameterizedSolverDTTests, DTTests, testing::ValuesIn(filter_solver_configurations({ THEORY_DATATYPE }))); diff --git a/tests/test-smtlib-reader.cpp b/tests/test-smtlib-reader.cpp index 6caf053ad..accd2f831 100644 --- a/tests/test-smtlib-reader.cpp +++ b/tests/test-smtlib-reader.cpp @@ -81,18 +81,6 @@ class IntReaderTests : public ReaderTests { }; -class BitVecReaderTests : public ReaderTests -{ -}; - -class ArrayIntReaderTests : public ReaderTests -{ -}; - -class UninterpReaderTests : public ReaderTests -{ -}; - TEST_P(IntReaderTests, QF_UFLIA_Smt2Files) { // SMT_SWITCH_DIR is a macro defined at build time @@ -112,63 +100,6 @@ TEST_P(IntReaderTests, QF_UFLIA_Smt2Files) } } -TEST_P(BitVecReaderTests, QF_UFBV_Smt2Files) -{ - // SMT_SWITCH_DIR is a macro defined at build time - // and should point to the top-level Smt-Switch directory - string test = STRFY(SMT_SWITCH_DIR); - auto testpair = get<1>(GetParam()); - test += "/tests/smt2/qf_ufbv/" + testpair.first; - reader->parse(test); - auto results = reader->get_results(); - auto expected_results = testpair.second; - ASSERT_EQ(results.size(), expected_results.size()); - - size_t size = results.size(); - for (size_t i = 0; i < size; i++) - { - EXPECT_EQ(results[i], expected_results[i]); - } -} - -TEST_P(ArrayIntReaderTests, QF_ALIA_Smt2Files) -{ - // SMT_SWITCH_DIR is a macro defined at build time - // and should point to the top-level Smt-Switch directory - string test = STRFY(SMT_SWITCH_DIR); - auto testpair = get<1>(GetParam()); - test += "/tests/smt2/qf_alia/" + testpair.first; - reader->parse(test); - auto results = reader->get_results(); - auto expected_results = testpair.second; - ASSERT_EQ(results.size(), expected_results.size()); - - size_t size = results.size(); - for (size_t i = 0; i < size; i++) - { - EXPECT_EQ(results[i], expected_results[i]); - } -} - -TEST_P(UninterpReaderTests, QF_UF_Smt2Files) -{ - // SMT_SWITCH_DIR is a macro defined at build time - // and should point to the top-level Smt-Switch directory - string test = STRFY(SMT_SWITCH_DIR); - auto testpair = get<1>(GetParam()); - test += "/tests/smt2/qf_uf/" + testpair.first; - reader->parse(test); - auto results = reader->get_results(); - auto expected_results = testpair.second; - ASSERT_EQ(results.size(), expected_results.size()); - - size_t size = results.size(); - for (size_t i = 0; i < size; i++) - { - EXPECT_EQ(results[i], expected_results[i]); - } -} - INSTANTIATE_TEST_SUITE_P( ParameterizedSolverIntReaderTests, IntReaderTests, @@ -177,35 +108,4 @@ INSTANTIATE_TEST_SUITE_P( testing::ValuesIn(qf_uflia_tests.begin(), qf_uflia_tests.end()))); -INSTANTIATE_TEST_SUITE_P( - ParameterizedSolverBitVecReaderTests, - BitVecReaderTests, - testing::Combine( - testing::ValuesIn(available_non_generic_solver_configurations()), - testing::ValuesIn(qf_ufbv_tests.begin(), qf_ufbv_tests.end()))); - -INSTANTIATE_TEST_SUITE_P( - ParameterizedSolverArrayIntReaderTests, - ArrayIntReaderTests, - testing::Combine(testing::ValuesIn(filter_non_generic_solver_configurations( - { THEORY_INT, ARRAY_MODELS })), - testing::ValuesIn(qf_alia_tests.begin(), - qf_alia_tests.end()))); - -INSTANTIATE_TEST_SUITE_P( - ParameterizedSolverUninterpReaderTests, - UninterpReaderTests, - testing::Combine(testing::ValuesIn(filter_non_generic_solver_configurations( - { UNINTERP_SORT })), - testing::ValuesIn(qf_uf_tests.begin(), - qf_uf_tests.end()))); - -INSTANTIATE_TEST_SUITE_P( - ParameterizedSolverParamUninterpReaderTests, - UninterpReaderTests, - testing::Combine(testing::ValuesIn(filter_non_generic_solver_configurations( - { PARAM_UNINTERP_SORT })), - testing::ValuesIn(qf_uf_param_sorts_tests.begin(), - qf_uf_param_sorts_tests.end()))); - } // namespace smt_tests