From: ajreynol Date: Thu, 2 Mar 2017 21:24:07 +0000 (-0600) Subject: Minor cleanup and reorganization related to last commit. X-Git-Tag: cvc5-1.0.0~5905 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=96b699bc6cccd1ade32e2d5ef73ce004063b8201;p=cvc5.git Minor cleanup and reorganization related to last commit. --- diff --git a/src/Makefile.am b/src/Makefile.am index 2ee777afe..c05065c35 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -117,16 +117,14 @@ libcvc4_la_SOURCES = \ prop/cryptominisat.cpp \ prop/theory_proxy.cpp \ prop/theory_proxy.h \ - smt/boolean_terms.cpp \ - smt/boolean_terms.h \ smt/command.cpp \ smt/command.h \ smt/command_list.cpp \ smt/command_list.h \ smt/dump.cpp \ smt/dump.h \ - smt/ite_removal.cpp \ - smt/ite_removal.h \ + smt/term_formula_removal.cpp \ + smt/term_formula_removal.h \ smt/logic_exception.h \ smt/logic_request.cpp \ smt/logic_request.h \ @@ -134,8 +132,6 @@ libcvc4_la_SOURCES = \ smt/managed_ostreams.h \ smt/model.cpp \ smt/model.h \ - smt/model_postprocessor.cpp \ - smt/model_postprocessor.h \ smt/smt_engine.cpp \ smt/smt_engine.h \ smt/smt_engine_check_proof.cpp \ diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h index 92d203cb3..66293d7ad 100644 --- a/src/decision/decision_engine.h +++ b/src/decision/decision_engine.h @@ -27,7 +27,7 @@ #include "prop/cnf_stream.h" #include "prop/prop_engine.h" #include "prop/sat_solver_types.h" -#include "smt/ite_removal.h" +#include "smt/term_formula_removal.h" #include "smt/smt_engine_scope.h" using namespace std; diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h index 591f018d8..5c3b01bef 100644 --- a/src/decision/decision_strategy.h +++ b/src/decision/decision_strategy.h @@ -20,7 +20,7 @@ #define __CVC4__DECISION__DECISION_STRATEGY_H #include "prop/sat_solver_types.h" -#include "smt/ite_removal.h" +#include "smt/term_formula_removal.h" namespace CVC4 { diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index c0d65cbe6..ded2cad15 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -22,7 +22,7 @@ #include "expr/node_manager.h" #include "options/decision_options.h" #include "theory/rewriter.h" -#include "smt/ite_removal.h" +#include "smt/term_formula_removal.h" #include "smt/smt_statistics_registry.h" namespace CVC4 { diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 1eb84b45f..31330a97c 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -216,8 +216,6 @@ liboptions_la_SOURCES = \ argument_extender_implementation.h \ argument_extender.h \ base_handlers.h \ - boolean_term_conversion_mode.cpp \ - boolean_term_conversion_mode.h \ bv_bitblast_mode.cpp \ bv_bitblast_mode.h \ decision_mode.cpp \ diff --git a/src/options/boolean_term_conversion_mode.cpp b/src/options/boolean_term_conversion_mode.cpp deleted file mode 100644 index 4fc9b1f8d..000000000 --- a/src/options/boolean_term_conversion_mode.cpp +++ /dev/null @@ -1,24 +0,0 @@ -/********************* */ -/*! \file boolean_term_conversion_mode.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ -#include "options/boolean_term_conversion_mode.h" - -#include - -namespace CVC4 { - - -}/* CVC4 namespace */ diff --git a/src/options/boolean_term_conversion_mode.h b/src/options/boolean_term_conversion_mode.h deleted file mode 100644 index 57e2ccaf4..000000000 --- a/src/options/boolean_term_conversion_mode.h +++ /dev/null @@ -1,34 +0,0 @@ -/********************* */ -/*! \file boolean_term_conversion_mode.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H -#define __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H - -#include - -namespace CVC4 { -namespace theory { -namespace booleans { - -}/* CVC4::theory::booleans namespace */ -}/* CVC4::theory namespace */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__BOOLEANS__BOOLEAN_TERM_CONVERSION_MODE_H */ diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index c0aa67cd4..94bf15540 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -32,7 +32,6 @@ #include "options/arith_propagation_mode.h" #include "options/arith_unate_lemma_mode.h" #include "options/base_options.h" -#include "options/boolean_term_conversion_mode.h" #include "options/bv_bitblast_mode.h" #include "options/bv_options.h" #include "options/decision_mode.h" diff --git a/src/options/options_handler.h b/src/options/options_handler.h index 248f15c98..6721eaa2b 100644 --- a/src/options/options_handler.h +++ b/src/options/options_handler.h @@ -27,7 +27,6 @@ #include "options/arith_propagation_mode.h" #include "options/arith_unate_lemma_mode.h" #include "options/base_handlers.h" -#include "options/boolean_term_conversion_mode.h" #include "options/bv_bitblast_mode.h" #include "options/decision_mode.h" #include "options/language.h" diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp deleted file mode 100644 index 442355580..000000000 --- a/src/smt/boolean_terms.cpp +++ /dev/null @@ -1,42 +0,0 @@ -/********************* */ -/*! \file boolean_terms.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ -#include "smt/boolean_terms.h" - -#include -#include -#include -#include -#include - -#include "expr/kind.h" -#include "expr/node_manager_attributes.h" -#include "options/boolean_term_conversion_mode.h" -#include "options/booleans_options.h" -#include "smt/smt_engine.h" -#include "theory/theory_engine.h" -#include "theory/theory_model.h" -#include "util/ntuple.h" - -using namespace std; -using namespace CVC4::theory; -using namespace CVC4::theory::booleans; - -namespace CVC4 { -namespace smt { - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h deleted file mode 100644 index 0fb82aafe..000000000 --- a/src/smt/boolean_terms.h +++ /dev/null @@ -1,32 +0,0 @@ -/********************* */ -/*! \file boolean_terms.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_private.h" - -#pragma once - -#include "expr/attribute.h" -#include "expr/node.h" -#include "util/hash.h" -#include -#include - -namespace CVC4 { -namespace smt { - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ diff --git a/src/smt/ite_removal.cpp b/src/smt/ite_removal.cpp deleted file mode 100644 index 0202a5a2d..000000000 --- a/src/smt/ite_removal.cpp +++ /dev/null @@ -1,235 +0,0 @@ -/********************* */ -/*! \file ite_removal.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 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 Removal of term ITEs - ** - ** Removal of term ITEs. - **/ -#include "smt/ite_removal.h" - -#include - -#include "options/proof_options.h" -#include "proof/proof_manager.h" -#include "theory/ite_utilities.h" - -using namespace std; - -namespace CVC4 { - -RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u) - : d_iteCache(u) -{ - d_containsVisitor = new theory::ContainsTermITEVisitor(); -} - -RemoveTermFormulas::~RemoveTermFormulas(){ - delete d_containsVisitor; -} - -void RemoveTermFormulas::garbageCollect(){ - d_containsVisitor->garbageCollect(); -} - -theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() { - return d_containsVisitor; -} - -size_t RemoveTermFormulas::collectedCacheSizes() const{ - return d_containsVisitor->cache_size() + d_iteCache.size(); -} - -void RemoveTermFormulas::run(std::vector& output, IteSkolemMap& iteSkolemMap, bool reportDeps) -{ - size_t n = output.size(); - for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { - // Do this in two steps to avoid Node problems(?) - // Appears related to bug 512, splitting this into two lines - // fixes the bug on clang on Mac OS - Node itesRemoved = run(output[i], output, iteSkolemMap, false, false); - // In some calling contexts, not necessary to report dependence information. - if (reportDeps && - (options::unsatCores() || options::fewerPreprocessingHoles())) { - // new assertions have a dependence on the node - PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); ) - while(n < output.size()) { - PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); ) - ++n; - } - } - output[i] = itesRemoved; - } -} - -bool RemoveTermFormulas::containsTermITE(TNode e) const { - return d_containsVisitor->containsTermITE(e); -} - -Node RemoveTermFormulas::run(TNode node, std::vector& output, - IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) { - // Current node - Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl; - - //if(node.isVar() || node.isConst()){ - // (options::biasedITERemoval() && !containsTermITE(node))){ - //if(node.isVar()){ - // return Node(node); - //} - if( node.getKind()==kind::INST_PATTERN_LIST ){ - return Node(node); - } - - // The result may be cached already - int cv = cacheVal( inQuant, inTerm ); - std::pair cacheKey(node, cv); - NodeManager *nodeManager = NodeManager::currentNM(); - ITECache::const_iterator i = d_iteCache.find(cacheKey); - if(i != d_iteCache.end()) { - Node cached = (*i).second; - Debug("ite") << "removeITEs: in-cache: " << cached << endl; - return cached.isNull() ? Node(node) : cached; - } - - - // If an ITE, replace it - TypeNode nodeType = node.getType(); - if(node.getKind() == kind::ITE) { - if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { - Node skolem; - // Make the skolem to represent the ITE - skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); - - // The new assertion - Node newAssertion = - nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), - skolem.eqNode(node[2])); - Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; - - // Attach the skolem - d_iteCache.insert(cacheKey, skolem); - - // Remove ITEs from the new assertion, rewrite it and push it to the output - newAssertion = run(newAssertion, output, iteSkolemMap, false, false); - - iteSkolemMap[skolem] = output.size(); - output.push_back(newAssertion); - - // The representation is now the skolem - return skolem; - } - } - //if a non-variable Boolean term, replace it - if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){ - Node skolem; - // Make the skolem to represent the Boolean term - //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal"); - skolem = nodeManager->mkBooleanTermVariable(); - - // The new assertion - Node newAssertion = skolem.eqNode( node ); - Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; - - // Attach the skolem - d_iteCache.insert(cacheKey, skolem); - - // Remove ITEs from the new assertion, rewrite it and push it to the output - newAssertion = run(newAssertion, output, iteSkolemMap, false, false); - - iteSkolemMap[skolem] = output.size(); - output.push_back(newAssertion); - - // The representation is now the skolem - return skolem; - } - - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { - // Remember if we're inside a quantifier - inQuant = true; - }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && - node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && - node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){ - // Remember if we're inside a term - Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl; - inTerm = true; - } - - // If not an ITE, go deep - vector newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - newChildren.push_back(node.getOperator()); - } - // Remove the ITEs from the children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = run(*it, output, iteSkolemMap, inQuant, inTerm); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } - - // If changes, we rewrite - if(somethingChanged) { - Node cached = nodeManager->mkNode(node.getKind(), newChildren); - d_iteCache.insert(cacheKey, cached); - return cached; - } else { - d_iteCache.insert(cacheKey, Node::null()); - return node; - } -} - -Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { - //if(node.isVar() || node.isConst()){ - // (options::biasedITERemoval() && !containsTermITE(node))){ - //if(node.isVar()){ - // return Node(node); - //} - if( node.getKind()==kind::INST_PATTERN_LIST ){ - return Node(node); - } - - // Check the cache - NodeManager *nodeManager = NodeManager::currentNM(); - int cv = cacheVal( inQuant, inTerm ); - ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv)); - if(i != d_iteCache.end()) { - Node cached = (*i).second; - return cached.isNull() ? Node(node) : cached; - } - - if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { - // Remember if we're inside a quantifier - inQuant = true; - }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){ - // Remember if we're inside a term - inTerm = true; - } - - vector newChildren; - bool somethingChanged = false; - if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { - newChildren.push_back(node.getOperator()); - } - // Replace in children - for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { - Node newChild = replace(*it, inQuant, inTerm); - somethingChanged |= (newChild != *it); - newChildren.push_back(newChild); - } - - // If changes, we rewrite - if(somethingChanged) { - return nodeManager->mkNode(node.getKind(), newChildren); - } else { - return node; - } -} - -}/* CVC4 namespace */ diff --git a/src/smt/ite_removal.h b/src/smt/ite_removal.h deleted file mode 100644 index e629c93d7..000000000 --- a/src/smt/ite_removal.h +++ /dev/null @@ -1,93 +0,0 @@ -/********************* */ -/*! \file ite_removal.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 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 Removal of term ITEs - ** - ** Removal of term ITEs. - **/ - -#include "cvc4_private.h" - -#pragma once - -#include - -#include "context/cdinsert_hashmap.h" -#include "context/context.h" -#include "expr/node.h" -#include "smt/dump.h" -#include "util/bool.h" -#include "util/hash.h" - -namespace CVC4 { - -namespace theory { - class ContainsTermITEVisitor; -}/* CVC4::theory namespace */ - -typedef std::hash_map IteSkolemMap; - -class RemoveTermFormulas { - typedef context::CDInsertHashMap< std::pair, Node, PairHashFunction > ITECache; - ITECache d_iteCache; - - static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); } -public: - - RemoveTermFormulas(context::UserContext* u); - ~RemoveTermFormulas(); - - /** - * Removes the ITE nodes by introducing skolem variables. All - * additional assertions are pushed into assertions. iteSkolemMap - * contains a map from introduced skolem variables to the index in - * assertions containing the new Boolean ite created in conjunction - * with that skolem variable. - * - * With reportDeps true, report reasoning dependences to the proof - * manager (for unsat cores). - */ - void run(std::vector& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false); - - /** - * Removes the ITE from the node by introducing skolem - * variables. All additional assertions are pushed into - * assertions. iteSkolemMap contains a map from introduced skolem - * variables to the index in assertions containing the new Boolean - * ite created in conjunction with that skolem variable. - */ - Node run(TNode node, std::vector& additionalAssertions, - IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm); - - /** - * Substitute under node using pre-existing cache. Do not remove - * any ITEs not seen during previous runs. - */ - Node replace(TNode node, bool inQuant = false, bool inTerm = false) const; - - /** Returns true if e contains a term ite. */ - bool containsTermITE(TNode e) const; - - /** Returns the collected size of the caches. */ - size_t collectedCacheSizes() const; - - /** Garbage collects non-context dependent data-structures. */ - void garbageCollect(); - - /** Return the RemoveTermFormulas's containsVisitor. */ - theory::ContainsTermITEVisitor* getContainsVisitor(); - -private: - theory::ContainsTermITEVisitor* d_containsVisitor; - -};/* class RemoveTTE */ - -}/* CVC4 namespace */ diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp deleted file mode 100644 index 0076b9de9..000000000 --- a/src/smt/model_postprocessor.cpp +++ /dev/null @@ -1,30 +0,0 @@ -/********************* */ -/*! \file model_postprocessor.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 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 - ** - ** - **/ - -#include "smt/model_postprocessor.h" - -#include "expr/node_manager_attributes.h" -#include "expr/record.h" -#include "smt/boolean_terms.h" - -using namespace std; - -namespace CVC4 { -namespace smt { - - -} /* namespace smt */ -} /* namespace CVC4 */ diff --git a/src/smt/model_postprocessor.h b/src/smt/model_postprocessor.h deleted file mode 100644 index a354315ef..000000000 --- a/src/smt/model_postprocessor.h +++ /dev/null @@ -1,31 +0,0 @@ -/********************* */ -/*! \file model_postprocessor.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2016 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 - ** - ** - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__MODEL_POSTPROCESSOR_H -#define __CVC4__MODEL_POSTPROCESSOR_H - -#include "expr/node.h" - -namespace CVC4 { -namespace smt { - - -}/* CVC4::smt namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__MODEL_POSTPROCESSOR_H */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cefef9345..b94e08fad 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -46,8 +46,6 @@ #include "options/arith_options.h" #include "options/arrays_options.h" #include "options/base_options.h" -#include "options/boolean_term_conversion_mode.h" -#include "options/booleans_options.h" #include "options/booleans_options.h" #include "options/bv_options.h" #include "options/datatypes_options.h" @@ -72,13 +70,11 @@ #include "proof/theory_proof.h" #include "proof/unsat_core.h" #include "prop/prop_engine.h" -#include "smt/boolean_terms.h" #include "smt/command.h" #include "smt/command_list.h" -#include "smt/ite_removal.h" +#include "smt/term_formula_removal.h" #include "smt/logic_request.h" #include "smt/managed_ostreams.h" -#include "smt/model_postprocessor.h" #include "smt/smt_engine_scope.h" #include "smt/update_ostream.h" #include "smt_util/boolean_simplification.h" @@ -4469,19 +4465,6 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec }/* SmtEngine::assertFormula() */ Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const { -/* - ModelPostprocessor mpost; - NodeVisitor visitor; - Node value = visitor.run(mpost, node); - Debug("boolean-terms") << "postproc: got " << value << " expect type " << expectedType << endl; - Node realValue = mpost.rewriteAs(value, expectedType); - Debug("boolean-terms") << "postproc: realval " << realValue << " expect type " << expectedType << endl; - if(options::condenseFunctionValues()) { - realValue = Rewriter::rewrite(realValue); - Debug("boolean-terms") << "postproc: after rewrite " << realValue << endl; - } - return realValue; - */ return node; } diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp new file mode 100644 index 000000000..3fd333cc5 --- /dev/null +++ b/src/smt/term_formula_removal.cpp @@ -0,0 +1,235 @@ +/********************* */ +/*! \file term_formula_removal.cpp + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 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 Removal of term formulas + ** + ** Removal of term formulas. + **/ +#include "smt/term_formula_removal.h" + +#include + +#include "options/proof_options.h" +#include "proof/proof_manager.h" +#include "theory/ite_utilities.h" + +using namespace std; + +namespace CVC4 { + +RemoveTermFormulas::RemoveTermFormulas(context::UserContext* u) + : d_iteCache(u) +{ + d_containsVisitor = new theory::ContainsTermITEVisitor(); +} + +RemoveTermFormulas::~RemoveTermFormulas(){ + delete d_containsVisitor; +} + +void RemoveTermFormulas::garbageCollect(){ + d_containsVisitor->garbageCollect(); +} + +theory::ContainsTermITEVisitor* RemoveTermFormulas::getContainsVisitor() { + return d_containsVisitor; +} + +size_t RemoveTermFormulas::collectedCacheSizes() const{ + return d_containsVisitor->cache_size() + d_iteCache.size(); +} + +void RemoveTermFormulas::run(std::vector& output, IteSkolemMap& iteSkolemMap, bool reportDeps) +{ + size_t n = output.size(); + for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) { + // Do this in two steps to avoid Node problems(?) + // Appears related to bug 512, splitting this into two lines + // fixes the bug on clang on Mac OS + Node itesRemoved = run(output[i], output, iteSkolemMap, false, false); + // In some calling contexts, not necessary to report dependence information. + if (reportDeps && + (options::unsatCores() || options::fewerPreprocessingHoles())) { + // new assertions have a dependence on the node + PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); ) + while(n < output.size()) { + PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); ) + ++n; + } + } + output[i] = itesRemoved; + } +} + +bool RemoveTermFormulas::containsTermITE(TNode e) const { + return d_containsVisitor->containsTermITE(e); +} + +Node RemoveTermFormulas::run(TNode node, std::vector& output, + IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm) { + // Current node + Debug("ite") << "removeITEs(" << node << ")" << " " << inQuant << " " << inTerm << endl; + + //if(node.isVar() || node.isConst()){ + // (options::biasedITERemoval() && !containsTermITE(node))){ + //if(node.isVar()){ + // return Node(node); + //} + if( node.getKind()==kind::INST_PATTERN_LIST ){ + return Node(node); + } + + // The result may be cached already + int cv = cacheVal( inQuant, inTerm ); + std::pair cacheKey(node, cv); + NodeManager *nodeManager = NodeManager::currentNM(); + ITECache::const_iterator i = d_iteCache.find(cacheKey); + if(i != d_iteCache.end()) { + Node cached = (*i).second; + Debug("ite") << "removeITEs: in-cache: " << cached << endl; + return cached.isNull() ? Node(node) : cached; + } + + + // If an ITE, replace it + TypeNode nodeType = node.getType(); + if(node.getKind() == kind::ITE) { + if(!nodeType.isBoolean() && (!inQuant || !node.hasBoundVar())) { + Node skolem; + // Make the skolem to represent the ITE + skolem = nodeManager->mkSkolem("termITE", nodeType, "a variable introduced due to term-level ITE removal"); + + // The new assertion + Node newAssertion = + nodeManager->mkNode(kind::ITE, node[0], skolem.eqNode(node[1]), + skolem.eqNode(node[2])); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the skolem + d_iteCache.insert(cacheKey, skolem); + + // Remove ITEs from the new assertion, rewrite it and push it to the output + newAssertion = run(newAssertion, output, iteSkolemMap, false, false); + + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); + + // The representation is now the skolem + return skolem; + } + } + //if a non-variable Boolean term, replace it + if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){ + Node skolem; + // Make the skolem to represent the Boolean term + //skolem = nodeManager->mkSkolem("termBT", nodeType, "a variable introduced due to Boolean term removal"); + skolem = nodeManager->mkBooleanTermVariable(); + + // The new assertion + Node newAssertion = skolem.eqNode( node ); + Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl; + + // Attach the skolem + d_iteCache.insert(cacheKey, skolem); + + // Remove ITEs from the new assertion, rewrite it and push it to the output + newAssertion = run(newAssertion, output, iteSkolemMap, false, false); + + iteSkolemMap[skolem] = output.size(); + output.push_back(newAssertion); + + // The representation is now the skolem + return skolem; + } + + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + // Remember if we're inside a quantifier + inQuant = true; + }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && + node.getKind()!=kind::EQUAL && node.getKind()!=kind::SEP_STAR && + node.getKind()!=kind::SEP_WAND && node.getKind()!=kind::SEP_LABEL ){ + // Remember if we're inside a term + Debug("ite") << "In term because of " << node << " " << node.getKind() << std::endl; + inTerm = true; + } + + // If not an ITE, go deep + vector newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Remove the ITEs from the children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = run(*it, output, iteSkolemMap, inQuant, inTerm); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + Node cached = nodeManager->mkNode(node.getKind(), newChildren); + d_iteCache.insert(cacheKey, cached); + return cached; + } else { + d_iteCache.insert(cacheKey, Node::null()); + return node; + } +} + +Node RemoveTermFormulas::replace(TNode node, bool inQuant, bool inTerm) const { + //if(node.isVar() || node.isConst()){ + // (options::biasedITERemoval() && !containsTermITE(node))){ + //if(node.isVar()){ + // return Node(node); + //} + if( node.getKind()==kind::INST_PATTERN_LIST ){ + return Node(node); + } + + // Check the cache + NodeManager *nodeManager = NodeManager::currentNM(); + int cv = cacheVal( inQuant, inTerm ); + ITECache::const_iterator i = d_iteCache.find(make_pair(node, cv)); + if(i != d_iteCache.end()) { + Node cached = (*i).second; + return cached.isNull() ? Node(node) : cached; + } + + if(node.getKind() == kind::FORALL || node.getKind() == kind::EXISTS) { + // Remember if we're inside a quantifier + inQuant = true; + }else if( theory::kindToTheoryId(node.getKind())!=theory::THEORY_BOOL && node.getKind()!=kind::EQUAL ){ + // Remember if we're inside a term + inTerm = true; + } + + vector newChildren; + bool somethingChanged = false; + if(node.getMetaKind() == kind::metakind::PARAMETERIZED) { + newChildren.push_back(node.getOperator()); + } + // Replace in children + for(TNode::const_iterator it = node.begin(), end = node.end(); it != end; ++it) { + Node newChild = replace(*it, inQuant, inTerm); + somethingChanged |= (newChild != *it); + newChildren.push_back(newChild); + } + + // If changes, we rewrite + if(somethingChanged) { + return nodeManager->mkNode(node.getKind(), newChildren); + } else { + return node; + } +} + +}/* CVC4 namespace */ diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h new file mode 100644 index 000000000..09991c571 --- /dev/null +++ b/src/smt/term_formula_removal.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \file term_formula_removal.h + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Dejan Jovanovic, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 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 Removal of term formulas + ** + ** Removal of term formulas. + **/ + +#include "cvc4_private.h" + +#pragma once + +#include + +#include "context/cdinsert_hashmap.h" +#include "context/context.h" +#include "expr/node.h" +#include "smt/dump.h" +#include "util/bool.h" +#include "util/hash.h" + +namespace CVC4 { + +namespace theory { + class ContainsTermITEVisitor; +}/* CVC4::theory namespace */ + +typedef std::hash_map IteSkolemMap; + +class RemoveTermFormulas { + typedef context::CDInsertHashMap< std::pair, Node, PairHashFunction > ITECache; + ITECache d_iteCache; + + static inline int cacheVal( bool inQuant, bool inTerm ) { return (inQuant ? 1 : 0) + 2*(inTerm ? 1 : 0); } +public: + + RemoveTermFormulas(context::UserContext* u); + ~RemoveTermFormulas(); + + /** + * Removes the ITE nodes by introducing skolem variables. All + * additional assertions are pushed into assertions. iteSkolemMap + * contains a map from introduced skolem variables to the index in + * assertions containing the new Boolean ite created in conjunction + * with that skolem variable. + * + * With reportDeps true, report reasoning dependences to the proof + * manager (for unsat cores). + */ + void run(std::vector& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false); + + /** + * Removes the ITE from the node by introducing skolem + * variables. All additional assertions are pushed into + * assertions. iteSkolemMap contains a map from introduced skolem + * variables to the index in assertions containing the new Boolean + * ite created in conjunction with that skolem variable. + */ + Node run(TNode node, std::vector& additionalAssertions, + IteSkolemMap& iteSkolemMap, bool inQuant, bool inTerm); + + /** + * Substitute under node using pre-existing cache. Do not remove + * any ITEs not seen during previous runs. + */ + Node replace(TNode node, bool inQuant = false, bool inTerm = false) const; + + /** Returns true if e contains a term ite. */ + bool containsTermITE(TNode e) const; + + /** Returns the collected size of the caches. */ + size_t collectedCacheSizes() const; + + /** Garbage collects non-context dependent data-structures. */ + void garbageCollect(); + + /** Return the RemoveTermFormulas's containsVisitor. */ + theory::ContainsTermITEVisitor* getContainsVisitor(); + +private: + theory::ContainsTermITEVisitor* d_containsVisitor; + +};/* class RemoveTTE */ + +}/* CVC4 namespace */ diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 8d2e5618f..b66cb15ff 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -23,7 +23,6 @@ #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" -#include "smt/boolean_terms.h" #include "theory/datatypes/datatypes_rewriter.h" #include "theory/datatypes/theory_datatypes_type_rules.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 3dacfca3a..adce94b5c 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -16,7 +16,7 @@ #include "theory/quantifiers/ceg_t_instantiator.h" #include "options/quantifiers_options.h" -#include "smt/ite_removal.h" +#include "smt/term_formula_removal.h" #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/term_database.h" #include "theory/quantifiers/quantifiers_rewriter.h" diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 0023f7d0f..1f1837740 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -14,7 +14,7 @@ #include "theory/quantifiers/inst_strategy_cbqi.h" #include "options/quantifiers_options.h" -#include "smt/ite_removal.h" +#include "smt/term_formula_removal.h" #include "theory/arith/partial_model.h" #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7c1b02f47..4054350aa 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -31,7 +31,7 @@ #include "proof/lemma_proof.h" #include "proof/proof_manager.h" #include "proof/theory_proof.h" -#include "smt/ite_removal.h" +#include "smt/term_formula_removal.h" #include "smt/logic_exception.h" #include "smt_util/lemma_output_channel.h" #include "smt_util/node_visitor.h"