diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:06:52 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-07-10 14:07:11 -0500 |
commit | f3590092818d9eab9d961ea602093029ff472a85 (patch) | |
tree | 1401f00df0d9659ba2321ea2088fe0c3f4de9f52 /src/compat/cvc3_compat.cpp | |
parent | d598a9644862d176632071bca8448765d9cc3cc1 (diff) |
Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
-rw-r--r-- | src/compat/cvc3_compat.cpp | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 1226d4db5..be24dacdd 100644 --- a/src/compat/cvc3_compat.cpp +++ b/src/compat/cvc3_compat.cpp @@ -1833,7 +1833,7 @@ Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field Type t = record.getType(); const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype(); unsigned index = CVC4::Datatype::indexOf( dt[0].getSelector(field) ); - return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), record); + return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( t, index ), record); } Expr ValidityChecker::recUpdateExpr(const Expr& record, const std::string& field, @@ -2236,8 +2236,9 @@ Expr ValidityChecker::tupleExpr(const std::vector<Expr>& exprs) { Expr ValidityChecker::tupleSelectExpr(const Expr& tuple, int index) { CompatCheckArgument(index >= 0 && index < ((CVC4::DatatypeType)tuple.getType()).getTupleLength(), "invalid index in tuple select"); - const CVC4::Datatype& dt = ((CVC4::DatatypeType)tuple.getType()).getDatatype(); - return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), tuple); + Type t = tuple.getType(); + const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype(); + return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal( t, index ), tuple); } Expr ValidityChecker::tupleUpdateExpr(const Expr& tuple, int index, @@ -2262,7 +2263,8 @@ Expr ValidityChecker::datatypeSelExpr(const std::string& selector, const Expr& a const CVC4::Datatype& dt = *(*i).second.first; string constructor = (*i).second.second; const CVC4::DatatypeConstructor& ctor = dt[constructor]; - return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR, ctor.getSelector(selector), arg); + unsigned sindex = CVC4::Datatype::indexOf( ctor.getSelector(selector) ); + return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR, ctor.getSelectorInternal( arg.getType(), sindex ), arg); } Expr ValidityChecker::datatypeTestExpr(const std::string& constructor, const Expr& arg) { |