From a2ccb633f0506ed6dd16a5da4a4a0a1efe0b4c9a Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Thu, 16 Aug 2018 23:01:05 -0500 Subject: [PATCH] Adding support for bitvector SyGuS problems without grammars (#2328) --- .../quantifiers/sygus/sygus_grammar_cons.cpp | 109 ++++++++++++++---- .../quantifiers/sygus/sygus_grammar_cons.h | 2 +- 2 files changed, 86 insertions(+), 25 deletions(-) diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index d6a6d0944..fbbfdec09 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -18,6 +18,7 @@ #include "expr/datatype.h" #include "options/quantifiers_options.h" +#include "theory/bv/theory_bv_utils.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/quantifiers/sygus/ce_guided_conjecture.h" #include "theory/quantifiers/sygus/sygus_grammar_norm.h" @@ -345,22 +346,27 @@ TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name, std::s return unresolved; } -void CegGrammarConstructor::mkSygusConstantsForType( TypeNode type, std::vector& ops ) { +void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, + std::vector& ops) +{ + NodeManager* nm = NodeManager::currentNM(); if (type.isReal()) { - ops.push_back(NodeManager::currentNM()->mkConst(Rational(0))); - ops.push_back(NodeManager::currentNM()->mkConst(Rational(1))); - }else if( type.isBitVector() ){ - unsigned sz = ((BitVectorType)type.toType()).getSize(); - BitVector bval0(sz, (unsigned int)0); - ops.push_back( NodeManager::currentNM()->mkConst(bval0) ); - BitVector bval1(sz, (unsigned int)1); - ops.push_back( NodeManager::currentNM()->mkConst(bval1) ); - }else if( type.isBoolean() ){ - ops.push_back(NodeManager::currentNM()->mkConst(true)); - ops.push_back(NodeManager::currentNM()->mkConst(false)); + ops.push_back(nm->mkConst(Rational(0))); + ops.push_back(nm->mkConst(Rational(1))); + } + else if (type.isBitVector()) + { + unsigned size = type.getBitVectorSize(); + ops.push_back(bv::utils::mkZero(size)); + ops.push_back(bv::utils::mkOne(size)); + } + else if (type.isBoolean()) + { + ops.push_back(nm->mkConst(true)); + ops.push_back(nm->mkConst(false)); } - //TODO : others? + // TODO #1178 : add other missing types } void CegGrammarConstructor::collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ){ @@ -494,7 +500,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( //ITE CVC4::Kind k = kind::ITE; Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + ops[i].push_back(nm->operatorOf(k).toExpr()); cnames.push_back( kind::kindToString(k) ); cargs.push_back( std::vector< CVC4::Type >() ); cargs.back().push_back(unres_bt); @@ -509,7 +515,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { Kind k = j == 0 ? PLUS : MINUS; Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + ops[i].push_back(nm->operatorOf(k).toExpr()); cnames.push_back(kind::kindToString(k)); cargs.push_back(std::vector()); cargs.back().push_back(unres_t); @@ -534,15 +540,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( std::vector> cargs_pos_int; /* Add operator 1 */ Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n"; - ops_pos_int.push_back( - NodeManager::currentNM()->mkConst(Rational(1)).toExpr()); + ops_pos_int.push_back(nm->mkConst(Rational(1)).toExpr()); ss << "_1"; cnames_pos_int.push_back(ss.str()); cargs_pos_int.push_back(std::vector()); /* Add operator PLUS */ Kind k = PLUS; Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n"; - ops_pos_int.push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + ops_pos_int.push_back(nm->operatorOf(k).toExpr()); cnames_pos_int.push_back(kindToString(k)); cargs_pos_int.push_back(std::vector()); cargs_pos_int.back().push_back(unres_pos_int_t); @@ -558,7 +563,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( /* Adding division at root */ k = DIVISION; Trace("sygus-grammar-def") << "\t...add for " << k << std::endl; - ops[i].push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + ops[i].push_back(nm->operatorOf(k).toExpr()); cnames.push_back(kindToString(k)); cargs.push_back(std::vector()); cargs.back().push_back(unres_t); @@ -566,7 +571,49 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( pcs.push_back(nullptr); weights.push_back(-1); } - }else if( types[i].isDatatype() ){ + } + else if (types[i].isBitVector()) + { + // unary apps + std::vector un_kinds = {BITVECTOR_NOT, BITVECTOR_NEG}; + for (const Kind k : un_kinds) + { + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + ops[i].push_back(nm->operatorOf(k).toExpr()); + cnames.push_back(kindToString(k)); + cargs.push_back(std::vector()); + cargs.back().push_back(unres_t); + pcs.push_back(nullptr); + weights.push_back(-1); + } + // binary apps + std::vector bin_kinds = {BITVECTOR_AND, + BITVECTOR_OR, + BITVECTOR_XOR, + BITVECTOR_PLUS, + BITVECTOR_SUB, + BITVECTOR_MULT, + BITVECTOR_UDIV_TOTAL, + BITVECTOR_UREM_TOTAL, + BITVECTOR_SDIV, + BITVECTOR_SREM, + BITVECTOR_SHL, + BITVECTOR_LSHR, + BITVECTOR_ASHR}; + for (const Kind k : bin_kinds) + { + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + ops[i].push_back(nm->operatorOf(k).toExpr()); + cnames.push_back(kindToString(k)); + cargs.push_back(std::vector()); + cargs.back().push_back(unres_t); + cargs.back().push_back(unres_t); + pcs.push_back(nullptr); + weights.push_back(-1); + } + } + else if (types[i].isDatatype()) + { Trace("sygus-grammar-def") << "...add for constructors" << std::endl; const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); for( unsigned k=0; kbooleanType(); + TypeNode btype = nm->booleanType(); datatypes.push_back(Datatype(dbname)); ops.push_back(std::vector()); std::vector cnames; @@ -672,7 +719,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( //add equality per type CVC4::Kind k = kind::EQUAL; Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + ops.back().push_back(nm->operatorOf(k).toExpr()); std::stringstream ss; ss << kind::kindToString(k) << "_" << types[i]; cnames.push_back(ss.str()); @@ -686,14 +733,28 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( { CVC4::Kind k = kind::LEQ; Trace("sygus-grammar-def") << "...add for " << k << std::endl; - ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr()); + ops.back().push_back(nm->operatorOf(k).toExpr()); cnames.push_back(kind::kindToString(k)); cargs.push_back( std::vector< CVC4::Type >() ); cargs.back().push_back(unres_types[i]); cargs.back().push_back(unres_types[i]); pcs.push_back(nullptr); weights.push_back(-1); - }else if( types[i].isDatatype() ){ + } + else if (types[i].isBitVector()) + { + Kind k = BITVECTOR_ULT; + Trace("sygus-grammar-def") << "...add for " << k << std::endl; + ops.back().push_back(nm->operatorOf(k).toExpr()); + cnames.push_back(kindToString(k)); + cargs.push_back(std::vector()); + cargs.back().push_back(unres_types[i]); + cargs.back().push_back(unres_types[i]); + pcs.push_back(nullptr); + weights.push_back(-1); + } + else if (types[i].isDatatype()) + { //add for testers Trace("sygus-grammar-def") << "...add for testers" << std::endl; const Datatype& dt = ((DatatypeType)types[i].toType()).getDatatype(); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index c99c431ea..84104e51c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -127,7 +127,7 @@ public: // helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction) static TypeNode mkUnresolvedType(const std::string& name, std::set& unres); // make the builtin constants for type type that should be included in a sygus grammar - static void mkSygusConstantsForType( TypeNode type, std::vector& ops ); + static void mkSygusConstantsForType(TypeNode type, std::vector& ops); // collect the list of types that depend on type range static void collectSygusGrammarTypesFor( TypeNode range, std::vector< TypeNode >& types, std::map< TypeNode, std::vector< DatatypeConstructorArg > >& sels ); /** helper function for function mkSygusDefaultType -- 2.30.2