diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 67 |
1 files changed, 0 insertions, 67 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index c4046b7c2..2fd61aabc 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -630,20 +630,6 @@ void Smt2::includeFile(const std::string& filename) { } } -void Smt2::mkSygusVar(const std::string& name, const Type& type, bool isPrimed) -{ - if (!isPrimed) - { - d_sygusVars.push_back(mkBoundVar(name, type)); - } -#ifdef CVC4_ASSERTIONS - else - { - d_sygusVarPrimed.push_back(mkBoundVar(name, type)); - } -#endif -} - void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) { if( type.isInteger() ){ ops.push_back(getExprManager()->mkConst(Rational(0))); @@ -1234,59 +1220,6 @@ Expr Smt2::makeSygusBoundVarList(Datatype& dt, return getExprManager()->mkExpr(kind::BOUND_VAR_LIST, lvars); } -const void Smt2::getSygusInvVars(FunctionType t, - std::vector<Expr>& vars, - std::vector<Expr>& primed_vars) -{ - std::vector<Type> argTypes = t.getArgTypes(); - ExprManager* em = getExprManager(); - for (const Type& ti : argTypes) - { - vars.push_back(em->mkBoundVar(ti)); - d_sygusVars.push_back(vars.back()); - std::stringstream ss; - ss << vars.back() << "'"; - primed_vars.push_back(em->mkBoundVar(ss.str(), ti)); - d_sygusVars.push_back(primed_vars.back()); -#ifdef CVC4_ASSERTIONS - bool find_new_declared_var = false; - for (const Expr& e : d_sygusVarPrimed) - { - if (e.getType() == ti) - { - d_sygusVarPrimed.erase( - std::find(d_sygusVarPrimed.begin(), d_sygusVarPrimed.end(), e)); - find_new_declared_var = true; - break; - } - } - if (!find_new_declared_var) - { - ss.str(""); - ss << "warning: decleared primed variables do not match invariant's " - "type\n"; - warning(ss.str()); - } -#endif - } -} - -const void Smt2::addSygusFunSymbol( Type t, Expr synth_fun ){ - // When constructing the synthesis conjecture, we quantify on the - // (higher-order) bound variable synth_fun. - d_sygusFunSymbols.push_back(synth_fun); - - // Variable "sfproxy" carries the type, which may be a SyGuS datatype - // that corresponds to syntactic restrictions. - Expr sym = mkBoundVar("sfproxy", t); - std::vector< Expr > attr_value; - attr_value.push_back(sym); - Command* cattr = - new SetUserAttributeCommand("sygus-synth-grammar", synth_fun, attr_value); - cattr->setMuted(true); - preemptCommand(cattr); -} - InputLanguage Smt2::getLanguage() const { ExprManager* em = getExprManager(); |