diff options
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/nl_ext_purify.cpp | 130 | ||||
-rw-r--r-- | src/preprocessing/passes/nl_ext_purify.h | 57 | ||||
-rw-r--r-- | src/preprocessing/passes/quantifier_macros.cpp | 550 | ||||
-rw-r--r-- | src/preprocessing/passes/quantifier_macros.h | 89 | ||||
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.cpp | 847 | ||||
-rw-r--r-- | src/preprocessing/passes/unconstrained_simplifier.h | 75 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass.h | 1 | ||||
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 3 |
8 files changed, 1752 insertions, 0 deletions
diff --git a/src/preprocessing/passes/nl_ext_purify.cpp b/src/preprocessing/passes/nl_ext_purify.cpp new file mode 100644 index 000000000..afb092571 --- /dev/null +++ b/src/preprocessing/passes/nl_ext_purify.cpp @@ -0,0 +1,130 @@ +/********************* */ +/*! \file nl_ext_purify.cpp + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The NlExtPurify preprocessing pass + ** + ** Purifies non-linear terms + **/ + +#include "preprocessing/passes/nl_ext_purify.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +Node NlExtPurify::purifyNlTerms(TNode n, + NodeMap& cache, + NodeMap& bcache, + std::vector<Node>& var_eq, + bool beneathMult) +{ + if (beneathMult) + { + NodeMap::iterator find = bcache.find(n); + if (find != bcache.end()) + { + return (*find).second; + } + } + else + { + NodeMap::iterator find = cache.find(n); + if (find != cache.end()) + { + return (*find).second; + } + } + Node ret = n; + if (n.getNumChildren() > 0) + { + if (beneathMult + && (n.getKind() == kind::PLUS || n.getKind() == kind::MINUS)) + { + // don't do it if it rewrites to a constant + Node nr = Rewriter::rewrite(n); + if (nr.isConst()) + { + // return the rewritten constant + ret = nr; + } + else + { + // new variable + ret = NodeManager::currentNM()->mkSkolem( + "__purifyNl_var", + n.getType(), + "Variable introduced in purifyNl pass"); + Node np = purifyNlTerms(n, cache, bcache, var_eq, false); + var_eq.push_back(np.eqNode(ret)); + Trace("nl-ext-purify") << "Purify : " << ret << " -> " << np + << std::endl; + } + } + else + { + bool beneathMultNew = beneathMult || n.getKind() == kind::MULT; + bool childChanged = false; + std::vector<Node> children; + for (unsigned i = 0, size = n.getNumChildren(); i < size; ++i) + { + Node nc = purifyNlTerms(n[i], cache, bcache, var_eq, beneathMultNew); + childChanged = childChanged || nc != n[i]; + children.push_back(nc); + } + if (childChanged) + { + ret = NodeManager::currentNM()->mkNode(n.getKind(), children); + } + } + } + if (beneathMult) + { + bcache[n] = ret; + } + else + { + cache[n] = ret; + } + return ret; +} + +NlExtPurify::NlExtPurify(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "nl-ext-purify"){}; + +PreprocessingPassResult NlExtPurify::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + unordered_map<Node, Node, NodeHashFunction> cache; + unordered_map<Node, Node, NodeHashFunction> bcache; + std::vector<Node> var_eq; + unsigned size = assertionsToPreprocess->size(); + for (unsigned i = 0; i < size; ++i) + { + Node a = (*assertionsToPreprocess)[i]; + assertionsToPreprocess->replace(i, purifyNlTerms(a, cache, bcache, var_eq)); + Trace("nl-ext-purify") << "Purify : " << a << " -> " + << (*assertionsToPreprocess)[i] << "\n"; + } + if (!var_eq.empty()) + { + unsigned lastIndex = size - 1; + var_eq.insert(var_eq.begin(), (*assertionsToPreprocess)[lastIndex]); + assertionsToPreprocess->replace( + lastIndex, NodeManager::currentNM()->mkNode(kind::AND, var_eq)); + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/nl_ext_purify.h b/src/preprocessing/passes/nl_ext_purify.h new file mode 100644 index 000000000..8d28b0742 --- /dev/null +++ b/src/preprocessing/passes/nl_ext_purify.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \file nl_ext_purify.h + ** \verbatim + ** Top contributors (to current version): + ** Haniel Barbosa + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief The NlExtPurify preprocessing pass + ** + ** Purifies non-linear terms by replacing sums under multiplications by fresh + ** variables + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H +#define __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H + +#include <unordered_map> +#include <vector> + +#include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>; + +class NlExtPurify : public PreprocessingPass +{ + public: + NlExtPurify(PreprocessingPassContext* preprocContext); + + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + Node purifyNlTerms(TNode n, + NodeMap& cache, + NodeMap& bcache, + std::vector<Node>& var_eq, + bool beneathMult = false); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif /* __CVC4__PREPROCESSING__PASSES__NL_EXT_PURIFY_H */ diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp new file mode 100644 index 000000000..e3bc02309 --- /dev/null +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -0,0 +1,550 @@ +/********************* */ +/*! \file quantifier_macros.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds, Tim King, Kshitij Bansal + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Sort inference module + ** + ** This class implements quantifiers macro definitions. + **/ + +#include "preprocessing/passes/quantifier_macros.h" + +#include <vector> + +#include "options/quantifiers_modes.h" +#include "options/quantifiers_options.h" +#include "proof/proof_manager.h" +#include "smt/smt_engine.h" +#include "smt/smt_engine_scope.h" +#include "theory/arith/arith_msum.h" +#include "theory/quantifiers/ematching/trigger.h" +#include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/term_util.h" +#include "theory/quantifiers_engine.h" +#include "theory/rewriter.h" + +using namespace std; +using namespace CVC4::theory; +using namespace CVC4::theory::quantifiers; +using namespace CVC4::kind; + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +QuantifierMacros::QuantifierMacros(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "quantifier-macros"), + d_ground_macros(false) +{ +} + +PreprocessingPassResult QuantifierMacros::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + bool success; + do + { + success = simplify(assertionsToPreprocess->ref(), true); + } while (success); + finalizeDefinitions(); + clearMaps(); + return PreprocessingPassResult::NO_CONFLICT; +} + +void QuantifierMacros::clearMaps() +{ + d_macro_basis.clear(); + d_macro_defs.clear(); + d_macro_defs_new.clear(); + d_macro_def_contains.clear(); + d_simplify_cache.clear(); + d_quant_macros.clear(); + d_ground_macros = false; +} + +bool QuantifierMacros::simplify( std::vector< Node >& assertions, bool doRewrite ){ + unsigned rmax = options::macrosQuantMode()==MACROS_QUANT_MODE_ALL ? 2 : 1; + for( unsigned r=0; r<rmax; r++ ){ + d_ground_macros = (r==0); + Trace("macros") << "Find macros, ground=" << d_ground_macros << "..." << std::endl; + //first, collect macro definitions + std::vector< Node > macro_assertions; + for( int i=0; i<(int)assertions.size(); i++ ){ + Trace("macros-debug") << " process assertion " << assertions[i] << std::endl; + if( processAssertion( assertions[i] ) ){ + PROOF( + if( std::find( macro_assertions.begin(), macro_assertions.end(), assertions[i] )==macro_assertions.end() ){ + macro_assertions.push_back( assertions[i] ); + } + ); + //process this assertion again + i--; + } + } + Trace("macros") << "...finished process, #new def = " << d_macro_defs_new.size() << std::endl; + if( doRewrite && !d_macro_defs_new.empty() ){ + bool retVal = false; + Trace("macros") << "Do simplifications..." << std::endl; + //now, rewrite based on macro definitions + for( unsigned i=0; i<assertions.size(); i++ ){ + Node curr = simplify( assertions[i] ); + if( curr!=assertions[i] ){ + curr = Rewriter::rewrite( curr ); + Trace("macros-rewrite") << "Rewrite " << assertions[i] << " to " << curr << std::endl; + //for now, it is dependent upon all assertions involving macros, this is an over-approximation. + //a more fine-grained unsat core computation would require caching dependencies for each subterm of the formula, + // which is expensive. + PROOF(ProofManager::currentPM()->addDependence(curr, assertions[i]); + for (unsigned j = 0; j < macro_assertions.size(); j++) { + if (macro_assertions[j] != assertions[i]) + { + ProofManager::currentPM()->addDependence( + curr, macro_assertions[j]); + } + }); + assertions[i] = curr; + retVal = true; + } + } + d_macro_defs_new.clear(); + if( retVal ){ + return true; + } + } + } + if( Trace.isOn("macros-warn") ){ + for( unsigned i=0; i<assertions.size(); i++ ){ + debugMacroDefinition( assertions[i], assertions[i] ); + } + } + return false; +} + +bool QuantifierMacros::processAssertion( Node n ) { + if( n.getKind()==AND ){ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( processAssertion( n[i] ) ){ + return true; + } + } + }else if( n.getKind()==FORALL && d_quant_macros.find( n )==d_quant_macros.end() ){ + std::vector< Node > args; + for( size_t j=0; j<n[0].getNumChildren(); j++ ){ + args.push_back( n[0][j] ); + } + Node nproc = n[1]; + if( !d_macro_defs_new.empty() ){ + nproc = simplify( nproc ); + if( nproc!=n[1] ){ + nproc = Rewriter::rewrite( nproc ); + } + } + //look at the body of the quantifier for macro definition + if( process( nproc, true, args, n ) ){ + d_quant_macros[n] = true; + return true; + } + } + return false; +} + +bool QuantifierMacros::containsBadOp( Node n, Node op, std::vector< Node >& opc, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==APPLY_UF ){ + Node nop = n.getOperator(); + if( nop==op || d_macro_defs.find( nop )!=d_macro_defs.end() ){ + return true; + } + if( std::find( opc.begin(), opc.end(), nop )==opc.end() ){ + opc.push_back( nop ); + } + }else if( d_ground_macros && n.getKind()==FORALL ){ + return true; + } + for( size_t i=0; i<n.getNumChildren(); i++ ){ + if( containsBadOp( n[i], op, opc, visited ) ){ + return true; + } + } + } + return false; +} + +bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ + return pol && n.getKind()==EQUAL; +} + +bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { + Node icn = d_preprocContext->getTheoryEngine() + ->getQuantifiersEngine() + ->getTermUtil() + ->substituteBoundVariablesToInstConstants(n, f); + Trace("macros-debug2") << "Get free variables in " << icn << std::endl; + std::vector< Node > var; + quantifiers::TermUtil::computeInstConstContainsForQuant(f, icn, var); + Trace("macros-debug2") << "Get trigger variables for " << icn << std::endl; + std::vector< Node > trigger_var; + inst::Trigger::getTriggerVariables( icn, f, trigger_var ); + Trace("macros-debug2") << "Done." << std::endl; + //only if all variables are also trigger variables + return trigger_var.size()>=var.size(); +} + +bool QuantifierMacros::isBoundVarApplyUf( Node n ) { + Assert( n.getKind()==APPLY_UF ); + TypeNode tno = n.getOperator().getType(); + std::map< Node, bool > vars; + // allow if a vector of unique variables of the same type as UF arguments + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + if( n[i].getKind()!=BOUND_VARIABLE ){ + return false; + } + if( n[i].getType()!=tno[i] ){ + return false; + } + if( vars.find( n[i] )==vars.end() ){ + vars[n[i]] = true; + }else{ + return false; + } + } + return true; +} + +void QuantifierMacros::getMacroCandidates( Node n, std::vector< Node >& candidates, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( n.getKind()==APPLY_UF ){ + if( isBoundVarApplyUf( n ) ){ + candidates.push_back( n ); + } + }else if( n.getKind()==PLUS ){ + for( size_t i=0; i<n.getNumChildren(); i++ ){ + getMacroCandidates( n[i], candidates, visited ); + } + }else if( n.getKind()==MULT ){ + //if the LHS is a constant + if( n.getNumChildren()==2 && n[0].isConst() ){ + getMacroCandidates( n[1], candidates, visited ); + } + }else if( n.getKind()==NOT ){ + getMacroCandidates( n[0], candidates, visited ); + } + } +} + +Node QuantifierMacros::solveInEquality( Node n, Node lit ){ + if( lit.getKind()==EQUAL ){ + //return the opposite side of the equality if defined that way + for( int i=0; i<2; i++ ){ + if( lit[i]==n ){ + return lit[i==0 ? 1 : 0]; + }else if( lit[i].getKind()==NOT && lit[i][0]==n ){ + return lit[i==0 ? 1 : 0].negate(); + } + } + std::map<Node, Node> msum; + if (ArithMSum::getMonomialSumLit(lit, msum)) + { + Node veq_c; + Node val; + int res = ArithMSum::isolate(n, msum, veq_c, val, EQUAL); + if (res != 0 && veq_c.isNull()) + { + return val; + } + } + } + Trace("macros-debug") << "Cannot find for " << lit << " " << n << std::endl; + return Node::null(); +} + +bool QuantifierMacros::getFreeVariables( Node n, std::vector< Node >& v_quant, std::vector< Node >& vars, bool retOnly, std::map< Node, bool >& visited ){ + if( visited.find( n )==visited.end() ){ + visited[n] = true; + if( std::find( v_quant.begin(), v_quant.end(), n )!=v_quant.end() ){ + if( std::find( vars.begin(), vars.end(), n )==vars.end() ){ + if( retOnly ){ + return true; + }else{ + vars.push_back( n ); + } + } + } + for( size_t i=0; i<n.getNumChildren(); i++ ){ + if( getFreeVariables( n[i], v_quant, vars, retOnly, visited ) ){ + return true; + } + } + } + return false; +} + +bool QuantifierMacros::getSubstitution( std::vector< Node >& v_quant, std::map< Node, Node >& solved, + std::vector< Node >& vars, std::vector< Node >& subs, bool reqComplete ){ + bool success = true; + for( size_t a=0; a<v_quant.size(); a++ ){ + if( !solved[ v_quant[a] ].isNull() ){ + vars.push_back( v_quant[a] ); + subs.push_back( solved[ v_quant[a] ] ); + }else{ + if( reqComplete ){ + success = false; + break; + } + } + } + return success; +} + +bool QuantifierMacros::process( Node n, bool pol, std::vector< Node >& args, Node f ){ + Trace("macros-debug") << " process " << n << std::endl; + if( n.getKind()==NOT ){ + return process( n[0], !pol, args, f ); + }else if( n.getKind()==AND || n.getKind()==OR ){ + //bool favorPol = (n.getKind()==AND)==pol; + //conditional? + }else if( n.getKind()==ITE ){ + //can not do anything + }else if( n.getKind()==APPLY_UF ){ + //predicate case + if( isBoundVarApplyUf( n ) ){ + Node op = n.getOperator(); + if( d_macro_defs.find( op )==d_macro_defs.end() ){ + Node n_def = NodeManager::currentNM()->mkConst( pol ); + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + std::stringstream ss; + ss << "mda_" << op << ""; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), n[i].getType(), "created during macro definition recognition" ); + d_macro_basis[op].push_back( v ); + } + //contains no ops + std::vector< Node > op_contains; + //add the macro + addMacro( op, n_def, op_contains ); + return true; + } + } + }else{ + //literal case + if( isMacroLiteral( n, pol ) ){ + Trace("macros-debug") << "Check macro literal : " << n << std::endl; + std::map< Node, bool > visited; + std::vector< Node > candidates; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + getMacroCandidates( n[i], candidates, visited ); + } + for( size_t i=0; i<candidates.size(); i++ ){ + Node m = candidates[i]; + Node op = m.getOperator(); + Trace("macros-debug") << "Check macro candidate : " << m << std::endl; + if( d_macro_defs.find( op )==d_macro_defs.end() ){ + std::vector< Node > fvs; + visited.clear(); + getFreeVariables( m, args, fvs, false, visited ); + //get definition and condition + Node n_def = solveInEquality( m, n ); //definition for the macro + if( !n_def.isNull() ){ + Trace("macros-debug") << m << " is possible macro in " << f << std::endl; + Trace("macros-debug") << " corresponding definition is : " << n_def << std::endl; + visited.clear(); + //definition must exist and not contain any free variables apart from fvs + if( !getFreeVariables( n_def, args, fvs, true, visited ) ){ + Trace("macros-debug") << "...free variables are contained." << std::endl; + visited.clear(); + //cannot contain a defined operator, opc is list of functions it contains + std::vector< Node > opc; + if( !containsBadOp( n_def, op, opc, visited ) ){ + Trace("macros-debug") << "...does not contain bad (recursive) operator." << std::endl; + //must be ground UF term if mode is GROUND_UF + if( options::macrosQuantMode()!=MACROS_QUANT_MODE_GROUND_UF || isGroundUfTerm( f, n_def ) ){ + Trace("macros-debug") << "...respects ground-uf constraint." << std::endl; + //now we must rewrite candidates[i] to a term of form g( x1, ..., xn ) where + // x1 ... xn are distinct variables + if( d_macro_basis[op].empty() ){ + for( size_t a=0; a<m.getNumChildren(); a++ ){ + std::stringstream ss; + ss << "mda_" << op << ""; + Node v = NodeManager::currentNM()->mkSkolem( ss.str(), m[a].getType(), "created during macro definition recognition" ); + d_macro_basis[op].push_back( v ); + } + } + std::map< Node, Node > solved; + for( size_t a=0; a<m.getNumChildren(); a++ ){ + solved[m[a]] = d_macro_basis[op][a]; + } + std::vector< Node > vars; + std::vector< Node > subs; + if( getSubstitution( fvs, solved, vars, subs, true ) ){ + n_def = n_def.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + addMacro( op, n_def, opc ); + return true; + } + } + } + } + } + } + } + } + } + return false; +} + +Node QuantifierMacros::simplify( Node n ){ + if( n.getNumChildren()==0 ){ + return n; + }else{ + std::map< Node, Node >::iterator itn = d_simplify_cache.find( n ); + if( itn!=d_simplify_cache.end() ){ + return itn->second; + }else{ + Node ret = n; + Trace("macros-debug") << " simplify " << n << std::endl; + std::vector< Node > children; + bool childChanged = false; + for( size_t i=0; i<n.getNumChildren(); i++ ){ + Node nn = simplify( n[i] ); + children.push_back( nn ); + childChanged = childChanged || nn!=n[i]; + } + bool retSet = false; + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + std::map< Node, Node >::iterator it = d_macro_defs.find( op ); + if( it!=d_macro_defs.end() && !it->second.isNull() ){ + //only apply if children are subtypes of arguments + bool success = true; + // FIXME : this can be eliminated when we have proper typing rules + std::vector< Node > cond; + TypeNode tno = op.getType(); + for( unsigned i=0; i<children.size(); i++ ){ + Node etc = TypeNode::getEnsureTypeCondition( children[i], tno[i] ); + if( etc.isNull() ){ + //if this does fail, we are incomplete, since we are eliminating quantified formula corresponding to op, + // and not ensuring it applies to n when its types are correct. + //Assert( false ); + success = false; + break; + }else if( !etc.isConst() ){ + cond.push_back( etc ); + } + Assert( children[i].getType().isSubtypeOf( tno[i] ) ); + } + if( success ){ + //do substitution if necessary + ret = it->second; + std::map< Node, std::vector< Node > >::iterator itb = d_macro_basis.find( op ); + if( itb!=d_macro_basis.end() ){ + ret = ret.substitute( itb->second.begin(), itb->second.end(), children.begin(), children.end() ); + } + if( !cond.empty() ){ + Node cc = cond.size()==1 ? cond[0] : NodeManager::currentNM()->mkNode( kind::AND, cond ); + ret = NodeManager::currentNM()->mkNode( kind::ITE, cc, ret, n ); + } + retSet = true; + } + } + } + if( !retSet && childChanged ){ + if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ + children.insert( children.begin(), n.getOperator() ); + } + ret = NodeManager::currentNM()->mkNode( n.getKind(), children ); + } + d_simplify_cache[n] = ret; + return ret; + } + } +} + +void QuantifierMacros::debugMacroDefinition( Node oo, Node n ) { + //for debugging, ensure that all previous definitions have been eliminated + if( n.getKind()==APPLY_UF ){ + Node op = n.getOperator(); + if( d_macro_defs.find( op )!=d_macro_defs.end() ){ + if( d_macro_defs.find( oo )!=d_macro_defs.end() ){ + Trace("macros-warn") << "BAD DEFINITION for macro " << oo << " : " << d_macro_defs[oo] << std::endl; + }else{ + Trace("macros-warn") << "BAD ASSERTION " << oo << std::endl; + } + Trace("macros-warn") << " contains defined function " << op << "!!!" << std::endl; + } + } + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + debugMacroDefinition( oo, n[i] ); + } +} + +void QuantifierMacros::finalizeDefinitions() { + bool doDefs = false; + if( Trace.isOn("macros-warn") ){ + doDefs = true; + } + if( options::incrementalSolving() || options::produceModels() || doDefs ){ + Trace("macros") << "Store as defined functions..." << std::endl; + //also store as defined functions + for( std::map< Node, Node >::iterator it = d_macro_defs.begin(); it != d_macro_defs.end(); ++it ){ + Trace("macros-def") << "Macro definition for " << it->first << " : " << it->second << std::endl; + Trace("macros-def") << " basis is : "; + std::vector< Node > nargs; + std::vector< Expr > args; + for( unsigned i=0; i<d_macro_basis[it->first].size(); i++ ){ + Node bv = NodeManager::currentNM()->mkBoundVar( d_macro_basis[it->first][i].getType() ); + Trace("macros-def") << d_macro_basis[it->first][i] << " "; + nargs.push_back( bv ); + args.push_back( bv.toExpr() ); + } + Trace("macros-def") << std::endl; + Node sbody = it->second.substitute( d_macro_basis[it->first].begin(), d_macro_basis[it->first].end(), nargs.begin(), nargs.end() ); + smt::currentSmtEngine()->defineFunction( it->first.toExpr(), args, sbody.toExpr() ); + + if( Trace.isOn("macros-warn") ){ + debugMacroDefinition( it->first, sbody ); + } + } + Trace("macros") << "done." << std::endl; + } +} + +void QuantifierMacros::addMacro( Node op, Node n, std::vector< Node >& opc ) { + Trace("macros") << "* " << n << " is a macro for " << op << ", #op contain = " << opc.size() << std::endl; + d_simplify_cache.clear(); + d_macro_defs[op] = n; + d_macro_defs_new[op] = n; + //substitute into all previous + std::vector< Node > dep_ops; + dep_ops.push_back( op ); + Trace("macros-debug") << "...substitute into " << d_macro_def_contains[op].size() << " previous definitions." << std::endl; + for( unsigned i=0; i<d_macro_def_contains[op].size(); i++ ){ + Node cop = d_macro_def_contains[op][i]; + Node def = d_macro_defs[cop]; + def = simplify( def ); + d_macro_defs[cop] = def; + if( d_macro_defs_new.find( cop )!=d_macro_defs_new.end() ){ + d_macro_defs_new[cop] = def; + } + dep_ops.push_back( cop ); + } + //store the contains op information + for( unsigned i=0; i<opc.size(); i++ ){ + for( unsigned j=0; j<dep_ops.size(); j++ ){ + Node dop = dep_ops[j]; + if( std::find( d_macro_def_contains[opc[i]].begin(), d_macro_def_contains[opc[i]].end(), dop )==d_macro_def_contains[opc[i]].end() ){ + d_macro_def_contains[opc[i]].push_back( dop ); + } + } + } +} + +} // passes +} // preprocessing +} // CVC4 diff --git a/src/preprocessing/passes/quantifier_macros.h b/src/preprocessing/passes/quantifier_macros.h new file mode 100644 index 000000000..092a62942 --- /dev/null +++ b/src/preprocessing/passes/quantifier_macros.h @@ -0,0 +1,89 @@ +/********************* */ +/*! \file quantifier_macros.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Pre-process step for detecting quantifier macro definitions + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H +#define __CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H + +#include <map> +#include <string> +#include <vector> +#include "expr/node.h" +#include "expr/type_node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class QuantifierMacros : public PreprocessingPass +{ + public: + QuantifierMacros(PreprocessingPassContext* preprocContext); + ~QuantifierMacros() {} + protected: + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + bool processAssertion(Node n); + bool isBoundVarApplyUf(Node n); + bool process(Node n, bool pol, std::vector<Node>& args, Node f); + bool containsBadOp(Node n, + Node op, + std::vector<Node>& opc, + std::map<Node, bool>& visited); + bool isMacroLiteral(Node n, bool pol); + bool isGroundUfTerm(Node f, Node n); + void getMacroCandidates(Node n, + std::vector<Node>& candidates, + std::map<Node, bool>& visited); + Node solveInEquality(Node n, Node lit); + bool getFreeVariables(Node n, + std::vector<Node>& v_quant, + std::vector<Node>& vars, + bool retOnly, + std::map<Node, bool>& visited); + bool getSubstitution(std::vector<Node>& v_quant, + std::map<Node, Node>& solved, + std::vector<Node>& vars, + std::vector<Node>& subs, + bool reqComplete); + void addMacro(Node op, Node n, std::vector<Node>& opc); + void debugMacroDefinition(Node oo, Node n); + bool simplify(std::vector<Node>& assertions, bool doRewrite = false); + Node simplify(Node n); + void finalizeDefinitions(); + void clearMaps(); + + // map from operators to macro basis terms + std::map<Node, std::vector<Node> > d_macro_basis; + // map from operators to macro definition + std::map<Node, Node> d_macro_defs; + std::map<Node, Node> d_macro_defs_new; + // operators to macro ops that contain them + std::map<Node, std::vector<Node> > d_macro_def_contains; + // simplify caches + std::map<Node, Node> d_simplify_cache; + std::map<Node, bool> d_quant_macros; + bool d_ground_macros; +}; + +} // passes +} // preprocessing +} // CVC4 + +#endif /*__CVC4__PREPROCESSING__PASSES__QUANTIFIER_MACROS_H */ diff --git a/src/preprocessing/passes/unconstrained_simplifier.cpp b/src/preprocessing/passes/unconstrained_simplifier.cpp new file mode 100644 index 000000000..6bb46f3f2 --- /dev/null +++ b/src/preprocessing/passes/unconstrained_simplifier.cpp @@ -0,0 +1,847 @@ +/********************* */ +/*! \file unconstrained_simplifier.cpp + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Tim King, Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Simplifications based on unconstrained variables + ** + ** This module implements a preprocessing phase which replaces certain + ** "unconstrained" expressions by variables. Based on Roberto + ** Bruttomesso's PhD thesis. + **/ + +#include "preprocessing/passes/unconstrained_simplifier.h" + +#include "smt/smt_statistics_registry.h" +#include "theory/logic_info.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +using namespace CVC4::theory; + +UnconstrainedSimplifier::UnconstrainedSimplifier( + PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "unconstrained-simplifier"), + d_numUnconstrainedElim("preprocessor::number of unconstrained elims", 0), + d_context(preprocContext->getDecisionContext()), + d_substitutions(preprocContext->getDecisionContext()), + d_logicInfo(preprocContext->getLogicInfo()) +{ + smtStatisticsRegistry()->registerStat(&d_numUnconstrainedElim); +} + +UnconstrainedSimplifier::~UnconstrainedSimplifier() +{ + smtStatisticsRegistry()->unregisterStat(&d_numUnconstrainedElim); +} + +struct unc_preprocess_stack_element +{ + TNode node; + TNode parent; + unc_preprocess_stack_element(TNode n) : node(n) {} + unc_preprocess_stack_element(TNode n, TNode p) : node(n), parent(p) {} +}; /* struct unc_preprocess_stack_element */ + +void UnconstrainedSimplifier::visitAll(TNode assertion) +{ + // Do a topological sort of the subexpressions and substitute them + vector<unc_preprocess_stack_element> toVisit; + toVisit.push_back(assertion); + + while (!toVisit.empty()) + { + // The current node we are processing + TNode current = toVisit.back().node; + TNode parent = toVisit.back().parent; + toVisit.pop_back(); + + TNodeCountMap::iterator find = d_visited.find(current); + if (find != d_visited.end()) + { + if (find->second == 1) + { + d_visitedOnce.erase(current); + if (current.isVar()) + { + d_unconstrained.erase(current); + } + } + ++find->second; + continue; + } + + d_visited[current] = 1; + d_visitedOnce[current] = parent; + + if (current.getNumChildren() == 0) + { + if (current.getKind() == kind::VARIABLE + || current.getKind() == kind::SKOLEM) + { + d_unconstrained.insert(current); + } + } + else + { + for (TNode childNode : current) + { + toVisit.push_back(unc_preprocess_stack_element(childNode, current)); + } + } + } +} + +Node UnconstrainedSimplifier::newUnconstrainedVar(TypeNode t, TNode var) +{ + Node n = NodeManager::currentNM()->mkSkolem( + "unconstrained", + t, + "a new var introduced because of unconstrained variable " + + var.toString()); + return n; +} + +void UnconstrainedSimplifier::processUnconstrained() +{ + NodeManager* nm = NodeManager::currentNM(); + + vector<TNode> workList(d_unconstrained.begin(), d_unconstrained.end()); + Node currentSub; + TNode parent; + bool swap; + bool isSigned; + bool strict; + vector<TNode> delayQueueLeft; + vector<Node> delayQueueRight; + + TNode current = workList.back(); + workList.pop_back(); + for (;;) + { + Assert(d_visitedOnce.find(current) != d_visitedOnce.end()); + parent = d_visitedOnce[current]; + if (!parent.isNull()) + { + swap = isSigned = strict = false; + bool checkParent = false; + switch (parent.getKind()) + { + // If-then-else operator - any two unconstrained children makes the + // parent unconstrained + case kind::ITE: + { + Assert(parent[0] == current || parent[1] == current + || parent[2] == current); + bool uCond = + parent[0] == current + || d_unconstrained.find(parent[0]) != d_unconstrained.end(); + bool uThen = + parent[1] == current + || d_unconstrained.find(parent[1]) != d_unconstrained.end(); + bool uElse = + parent[2] == current + || d_unconstrained.find(parent[2]) != d_unconstrained.end(); + if ((uCond && uThen) || (uCond && uElse) || (uThen && uElse)) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + ++d_numUnconstrainedElim; + if (uThen) + { + if (parent[1] != current) + { + if (parent[1].isVar()) + { + currentSub = parent[1]; + } + else + { + Assert(d_substitutions.hasSubstitution(parent[1])); + currentSub = d_substitutions.apply(parent[1]); + } + } + else if (currentSub.isNull()) + { + currentSub = current; + } + } + else if (parent[2] != current) + { + if (parent[2].isVar()) + { + currentSub = parent[2]; + } + else + { + Assert(d_substitutions.hasSubstitution(parent[2])); + currentSub = d_substitutions.apply(parent[2]); + } + } + else if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + } + else + { + currentSub = Node(); + } + } + else if (uCond) + { + Cardinality card = parent.getType().getCardinality(); + if (card.isFinite() && !card.isLargeFinite() + && card.getFiniteCardinality() == 2) + { + // Special case: condition is unconstrained, then and else are + // different, and total cardinality of the type is 2, then the + // result is unconstrained + Node test = Rewriter::rewrite(parent[1].eqNode(parent[2])); + if (test == nm->mkConst<bool>(false)) + { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + } + } + } + break; + } + + // Comparisons that return a different type - assuming domains are + // larger than 1, any unconstrained child makes parent unconstrained as + // well + case kind::EQUAL: + if (parent[0].getType() != parent[1].getType()) + { + TNode other = (parent[0] == current) ? parent[1] : parent[0]; + if (current.getType().isSubtypeOf(other.getType())) + { + break; + } + } + if (parent[0].getType().isDatatype()) + { + TypeNode tn = parent[0].getType(); + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + if (dt.isRecursiveSingleton(tn.toType())) + { + // domain size may be 1 + break; + } + } + if (parent[0].getType().isBoolean()) + { + checkParent = true; + break; + } + case kind::BITVECTOR_COMP: + case kind::LT: + case kind::LEQ: + case kind::GT: + case kind::GEQ: + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + ++d_numUnconstrainedElim; + Assert(parent[0] != parent[1] + && (parent[0] == current || parent[1] == current)); + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + } + else + { + currentSub = Node(); + } + break; + } + + // Unary operators that propagate unconstrainedness + case kind::NOT: + case kind::BITVECTOR_NOT: + case kind::BITVECTOR_NEG: + case kind::UMINUS: + ++d_numUnconstrainedElim; + Assert(parent[0] == current); + if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + break; + + // Unary operators that propagate unconstrainedness and return a + // different type + case kind::BITVECTOR_EXTRACT: + ++d_numUnconstrainedElim; + Assert(parent[0] == current); + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + break; + + // Operators returning same type requiring all children to be + // unconstrained + case kind::AND: + case kind::OR: + case kind::IMPLIES: + case kind::BITVECTOR_AND: + case kind::BITVECTOR_OR: + case kind::BITVECTOR_NAND: + case kind::BITVECTOR_NOR: + { + bool allUnconstrained = true; + for (TNode child : parent) + { + if (d_unconstrained.find(child) == d_unconstrained.end()) + { + allUnconstrained = false; + break; + } + } + if (allUnconstrained) + { + checkParent = true; + } + } + break; + + // Require all children to be unconstrained and different + case kind::BITVECTOR_SHL: + case kind::BITVECTOR_LSHR: + case kind::BITVECTOR_ASHR: + case kind::BITVECTOR_UDIV_TOTAL: + case kind::BITVECTOR_UREM_TOTAL: + case kind::BITVECTOR_SDIV: + case kind::BITVECTOR_SREM: + case kind::BITVECTOR_SMOD: + { + bool allUnconstrained = true; + bool allDifferent = true; + for (TNode::iterator child_it = parent.begin(); + child_it != parent.end(); + ++child_it) + { + if (d_unconstrained.find(*child_it) == d_unconstrained.end()) + { + allUnconstrained = false; + break; + } + for (TNode::iterator child_it2 = child_it + 1; + child_it2 != parent.end(); + ++child_it2) + { + if (*child_it == *child_it2) + { + allDifferent = false; + break; + } + } + } + if (allUnconstrained && allDifferent) + { + checkParent = true; + } + break; + } + + // Requires all children to be unconstrained and different, and returns + // a different type + case kind::BITVECTOR_CONCAT: + { + bool allUnconstrained = true; + bool allDifferent = true; + for (TNode::iterator child_it = parent.begin(); + child_it != parent.end(); + ++child_it) + { + if (d_unconstrained.find(*child_it) == d_unconstrained.end()) + { + allUnconstrained = false; + break; + } + for (TNode::iterator child_it2 = child_it + 1; + child_it2 != parent.end(); + ++child_it2) + { + if (*child_it == *child_it2) + { + allDifferent = false; + break; + } + } + } + if (allUnconstrained && allDifferent) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + } + else + { + currentSub = Node(); + } + } + } + break; + + // N-ary operators returning same type requiring at least one child to + // be unconstrained + case kind::PLUS: + case kind::MINUS: + if (current.getType().isInteger() && !parent.getType().isInteger()) + { + break; + } + case kind::XOR: + case kind::BITVECTOR_XOR: + case kind::BITVECTOR_XNOR: + case kind::BITVECTOR_PLUS: + case kind::BITVECTOR_SUB: checkParent = true; break; + + // Multiplication/division: must be non-integer and other operand must + // be non-zero + case kind::MULT: + case kind::DIVISION: + { + Assert(parent.getNumChildren() == 2); + TNode other; + if (parent[0] == current) + { + other = parent[1]; + } + else + { + Assert(parent[1] == current); + other = parent[0]; + } + if (d_unconstrained.find(other) != d_unconstrained.end()) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + if (current.getType().isInteger() && other.getType().isInteger()) + { + Assert(parent.getKind() == kind::DIVISION + || parent.getType().isInteger()); + if (parent.getKind() == kind::DIVISION) + { + break; + } + } + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + } + else + { + currentSub = Node(); + } + } + else + { + // if only the denominator of a division is unconstrained, can't + // set it to 0 so the result is not unconstrained + if (parent.getKind() == kind::DIVISION && current == parent[1]) + { + break; + } + // if we are an integer, the only way we are unconstrained is if + // we are a MULT by -1 + if (current.getType().isInteger()) + { + // div/mult by 1 should have been simplified + Assert(other != nm->mkConst<Rational>(1)); + // div by -1 should have been simplified + if (other != nm->mkConst<Rational>(-1)) + { + break; + } + else + { + Assert(parent.getKind() == kind::MULT); + Assert(parent.getType().isInteger()); + } + } + else + { + // TODO(#2377): could build ITE here + Node test = other.eqNode(nm->mkConst<Rational>(0)); + if (Rewriter::rewrite(test) != nm->mkConst<bool>(false)) + { + break; + } + } + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + } + break; + } + + // Bitvector MULT - current must only appear once in the children: + // all other children must be unconstrained or odd + case kind::BITVECTOR_MULT: + { + bool found = false; + bool done = false; + + for (TNode child : parent) + { + if (child == current) + { + if (found) + { + done = true; + break; + } + found = true; + continue; + } + else if (d_unconstrained.find(child) == d_unconstrained.end()) + { + Node extractOp = + nm->mkConst<BitVectorExtract>(BitVectorExtract(0, 0)); + vector<Node> children; + children.push_back(child); + Node test = nm->mkNode(extractOp, children); + BitVector one(1, unsigned(1)); + test = test.eqNode(nm->mkConst<BitVector>(one)); + if (Rewriter::rewrite(test) != nm->mkConst<bool>(true)) + { + done = true; + break; + } + } + } + if (done) + { + break; + } + checkParent = true; + break; + } + + // Uninterpreted function - if domain is infinite, no quantifiers are + // used, and any child is unconstrained, result is unconstrained + case kind::APPLY_UF: + if (d_logicInfo.isQuantified() + || !current.getType().getCardinality().isInfinite()) + { + break; + } + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + if (parent.getType() != current.getType()) + { + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + } + current = parent; + } + else + { + currentSub = Node(); + } + break; + + // Array select - if array is unconstrained, so is result + case kind::SELECT: + if (parent[0] == current) + { + ++d_numUnconstrainedElim; + Assert(current.getType().isArray()); + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar( + current.getType().getArrayConstituentType(), currentSub); + current = parent; + } + break; + + // Array store - if both store and value are unconstrained, so is + // resulting store + case kind::STORE: + if (((parent[0] == current + && d_unconstrained.find(parent[2]) != d_unconstrained.end()) + || (parent[2] == current + && d_unconstrained.find(parent[0]) + != d_unconstrained.end()))) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + ++d_numUnconstrainedElim; + if (parent[0] != current) + { + if (parent[0].isVar()) + { + currentSub = parent[0]; + } + else + { + Assert(d_substitutions.hasSubstitution(parent[0])); + currentSub = d_substitutions.apply(parent[0]); + } + } + else if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + } + else + { + currentSub = Node(); + } + } + break; + + // Bit-vector comparisons: replace with new Boolean variable, but have + // to also conjoin with a side condition as there is always one case + // when the comparison is forced to be false + case kind::BITVECTOR_ULT: + case kind::BITVECTOR_UGE: + case kind::BITVECTOR_UGT: + case kind::BITVECTOR_ULE: + case kind::BITVECTOR_SLT: + case kind::BITVECTOR_SGE: + case kind::BITVECTOR_SGT: + case kind::BITVECTOR_SLE: + { + // Tuples over (signed, swap, strict). + switch (parent.getKind()) + { + case kind::BITVECTOR_UGE: break; + case kind::BITVECTOR_ULT: strict = true; break; + case kind::BITVECTOR_ULE: swap = true; break; + case kind::BITVECTOR_UGT: + swap = true; + strict = true; + break; + case kind::BITVECTOR_SGE: isSigned = true; break; + case kind::BITVECTOR_SLT: + isSigned = true; + strict = true; + break; + case kind::BITVECTOR_SLE: + isSigned = true; + swap = true; + break; + case kind::BITVECTOR_SGT: + isSigned = true; + swap = true; + strict = true; + break; + default: Unreachable(); + } + TNode other; + bool left = false; + if (parent[0] == current) + { + other = parent[1]; + left = true; + } + else + { + Assert(parent[1] == current); + other = parent[0]; + } + if (d_unconstrained.find(other) != d_unconstrained.end()) + { + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + } + else + { + currentSub = Node(); + } + } + else + { + unsigned size = current.getType().getBitVectorSize(); + BitVector bv = + isSigned ? BitVector(size, Integer(1).multiplyByPow2(size - 1)) + : BitVector(size, unsigned(0)); + if (swap == left) + { + bv = ~bv; + } + if (currentSub.isNull()) + { + currentSub = current; + } + currentSub = newUnconstrainedVar(parent.getType(), currentSub); + current = parent; + Node test = + Rewriter::rewrite(other.eqNode(nm->mkConst<BitVector>(bv))); + if (test == nm->mkConst<bool>(false)) + { + break; + } + currentSub = strict ? currentSub.andNode(test.notNode()) + : currentSub.orNode(test); + // Delay adding this substitution - see comment at end of function + delayQueueLeft.push_back(current); + delayQueueRight.push_back(currentSub); + currentSub = Node(); + parent = TNode(); + } + break; + } + + // Do nothing + case kind::BITVECTOR_SIGN_EXTEND: + case kind::BITVECTOR_ZERO_EXTEND: + case kind::BITVECTOR_REPEAT: + case kind::BITVECTOR_ROTATE_LEFT: + case kind::BITVECTOR_ROTATE_RIGHT: + + default: break; + } + if (checkParent) + { + // run for various cases from above + if (d_unconstrained.find(parent) == d_unconstrained.end() + && !d_substitutions.hasSubstitution(parent)) + { + ++d_numUnconstrainedElim; + if (currentSub.isNull()) + { + currentSub = current; + } + current = parent; + } + else + { + currentSub = Node(); + } + } + if (current == parent && d_visited[parent] == 1) + { + d_unconstrained.insert(parent); + continue; + } + } + if (!currentSub.isNull()) + { + Assert(currentSub.isVar()); + d_substitutions.addSubstitution(current, currentSub, false); + } + if (workList.empty()) + { + break; + } + current = workList.back(); + currentSub = Node(); + workList.pop_back(); + } + TNode left; + Node right; + // All substitutions except those arising from bitvector comparisons are + // substitutions t -> x where x is a variable. This allows us to build the + // substitution very quickly (never invalidating the substitution cache). + // Bitvector comparisons are more complicated and may require + // back-substitution and cache-invalidation. So we do these last. + while (!delayQueueLeft.empty()) + { + left = delayQueueLeft.back(); + if (!d_substitutions.hasSubstitution(left)) + { + right = d_substitutions.apply(delayQueueRight.back()); + d_substitutions.addSubstitution(delayQueueLeft.back(), right); + } + delayQueueLeft.pop_back(); + delayQueueRight.pop_back(); + } +} + +PreprocessingPassResult UnconstrainedSimplifier::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + d_preprocContext->spendResource(options::preprocessStep()); + + std::vector<Node>& assertions = assertionsToPreprocess->ref(); + + d_context->push(); + + for (const Node& assertion : assertions) + { + visitAll(assertion); + } + + if (!d_unconstrained.empty()) + { + processUnconstrained(); + // d_substitutions.print(Message.getStream()); + for (Node& assertion : assertions) + { + assertion = Rewriter::rewrite(d_substitutions.apply(assertion)); + } + } + + // to clear substitutions map + d_context->pop(); + + d_visited.clear(); + d_visitedOnce.clear(); + d_unconstrained.clear(); + + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/unconstrained_simplifier.h b/src/preprocessing/passes/unconstrained_simplifier.h new file mode 100644 index 000000000..658834ee3 --- /dev/null +++ b/src/preprocessing/passes/unconstrained_simplifier.h @@ -0,0 +1,75 @@ +/********************* */ +/*! \file unconstrained_simplifier.h + ** \verbatim + ** Top contributors (to current version): + ** Clark Barrett, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Simplifications based on unconstrained variables + ** + ** This module implements a preprocessing phase which replaces certain + ** "unconstrained" expressions by variables. Based on Roberto + ** Bruttomesso's PhD thesis. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H +#define __CVC4__PREPROCESSING_PASSES_UNCONSTRAINED_SIMPLIFIER_H + +#include <unordered_map> +#include <unordered_set> +#include <vector> + +#include "context/context.h" +#include "expr/node.h" +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" +#include "theory/logic_info.h" +#include "theory/substitutions.h" +#include "util/statistics_registry.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class UnconstrainedSimplifier : public PreprocessingPass +{ + public: + UnconstrainedSimplifier(PreprocessingPassContext* preprocContext); + ~UnconstrainedSimplifier() override; + + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; + + private: + /** number of expressions eliminated due to unconstrained simplification */ + IntStat d_numUnconstrainedElim; + + using TNodeCountMap = std::unordered_map<TNode, unsigned, TNodeHashFunction>; + using TNodeMap = std::unordered_map<TNode, TNode, TNodeHashFunction>; + using TNodeSet = std::unordered_set<TNode, TNodeHashFunction>; + + TNodeCountMap d_visited; + TNodeMap d_visitedOnce; + TNodeSet d_unconstrained; + + context::Context* d_context; + theory::SubstitutionMap d_substitutions; + + const LogicInfo& d_logicInfo; + + void visitAll(TNode assertion); + Node newUnconstrainedVar(TypeNode t, TNode var); + void processUnconstrained(); +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index 97fa32d17..4143f2d4b 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -39,6 +39,7 @@ #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_engine_scope.h" #include "smt/term_formula_removal.h" +#include "theory/logic_info.h" #include "theory/substitutions.h" namespace CVC4 { diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index a289752fa..96e554680 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -43,6 +43,7 @@ class PreprocessingPassContext DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; } prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; } context::Context* getUserContext() { return d_smt->d_userContext; } + context::Context* getDecisionContext() { return d_smt->d_context; } RemoveTermFormulas* getIteRemover() { return d_iteRemover; } void spendResource(unsigned amount) @@ -50,6 +51,8 @@ class PreprocessingPassContext d_resourceManager->spendResource(amount); } + const LogicInfo& getLogicInfo() { return d_smt->d_logic; } + /* Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); |