diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-10 15:51:25 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-10 13:51:25 -0700 |
commit | 7e9b3dfa40f0297bdb005f6c802443ebb3b8cad1 (patch) | |
tree | be4db1f4485a4722a7c816edee708c57d676b5ba /src | |
parent | 1dbc8aa695772daf2c83d10a7adb8123f97fa16f (diff) |
Front end support for integer AND (#4717)
Diffstat (limited to 'src')
-rw-r--r-- | src/api/cvc4cpp.cpp | 9 | ||||
-rw-r--r-- | src/api/cvc4cppkind.h | 17 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 5 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 5 |
4 files changed, 36 insertions, 0 deletions
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index a04b5cf85..ebafc3cc8 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -98,6 +98,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{ /* Arithmetic ---------------------------------------------------------- */ {PLUS, CVC4::Kind::PLUS}, {MULT, CVC4::Kind::MULT}, + {IAND, CVC4::Kind::IAND}, {MINUS, CVC4::Kind::MINUS}, {UMINUS, CVC4::Kind::UMINUS}, {DIVISION, CVC4::Kind::DIVISION}, @@ -348,6 +349,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> /* Arithmetic ------------------------------------------------------ */ {CVC4::Kind::PLUS, PLUS}, {CVC4::Kind::MULT, MULT}, + {CVC4::Kind::IAND, IAND}, {CVC4::Kind::MINUS, MINUS}, {CVC4::Kind::UMINUS, UMINUS}, {CVC4::Kind::DIVISION, DIVISION}, @@ -593,6 +595,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction> const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds( {RECORD_UPDATE, DIVISIBLE, + IAND, BITVECTOR_REPEAT, BITVECTOR_ZERO_EXTEND, BITVECTOR_SIGN_EXTEND, @@ -1262,6 +1265,7 @@ uint32_t Op::getIndices() const i = d_expr->getConst<BitVectorRotateRight>().d_rotateRightAmount; break; case INT_TO_BITVECTOR: i = d_expr->getConst<IntToBitVector>().d_size; break; + case IAND: i = d_expr->getConst<IntAnd>().d_size; break; case FLOATINGPOINT_TO_UBV: i = d_expr->getConst<FloatingPointToUBV>().bvs.d_size; break; @@ -4019,6 +4023,11 @@ Op Solver::mkOp(Kind kind, uint32_t arg) const *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)) .d_expr.get()); break; + case IAND: + res = Op(this, + kind, + *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_expr.get()); + break; case FLOATINGPOINT_TO_UBV: res = Op( this, diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h index b3e88c98c..1f23d0e8d 100644 --- a/src/api/cvc4cppkind.h +++ b/src/api/cvc4cppkind.h @@ -319,6 +319,23 @@ enum CVC4_PUBLIC Kind : int32_t * mkTerm(Kind kind, const std::vector<Term>& children) */ MULT, + /** + * Operator for Integer AND + * Parameter: 1 + * -[1]: Size of the bit-vector that determines the semantics of the IAND + * Create with: + * mkOp(Kind kind, uint32_t param). + * + * Apply integer conversion to bit-vector. + * Parameters: 2 + * -[1]: Op of kind IAND + * -[2]: Integer term + * -[3]: Integer term + * Create with: + * mkTerm(Op op, Term child1, Term child2) + * mkTerm(Op op, const std::vector<Term>& children) + */ + IAND, #if 0 /* Synonym for MULT. */ NONLINEAR_MULT, diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 46a2e2c59..ec2009cc3 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -639,6 +639,11 @@ Command* Smt2::setLogic(std::string name, bool fromCommand) defineVar("real.pi", d_solver->mkTerm(api::PI)); addTranscendentalOperators(); } + if (!strictModeEnabled()) + { + // integer version of AND + addIndexedOperator(api::IAND, api::IAND, "iand"); + } } if(d_logic.isTheoryEnabled(theory::THEORY_ARRAYS)) { diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6077601bc..773c733d6 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -601,6 +601,10 @@ void Smt2Printer::toStream(std::ostream& out, parametricTypeChildren = true; out << smtKindString(k, d_variant) << " "; break; + case kind::IAND: + out << "(_ iand " << n.getOperator().getConst<IntAnd>().d_size << ") "; + stillNeedToPrintParams = false; + break; case kind::DIVISIBLE: out << "(_ divisible " << n.getOperator().getConst<Divisible>().k << ")"; @@ -1031,6 +1035,7 @@ static string smtKindString(Kind k, Variant v) case kind::PLUS: return "+"; case kind::MULT: case kind::NONLINEAR_MULT: return "*"; + case kind::IAND: return "iand"; case kind::EXPONENTIAL: return "exp"; case kind::SINE: return "sin"; case kind::COSINE: return "cos"; |