diff options
Diffstat (limited to 'src/theory/quantifiers')
163 files changed, 1270 insertions, 864 deletions
diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp index 577b2c31f..bb0cdde83 100644 --- a/src/theory/quantifiers/alpha_equivalence.cpp +++ b/src/theory/quantifiers/alpha_equivalence.cpp @@ -2,9 +2,9 @@ /*! \file alpha_equivalence.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h index 4ab45b015..b5d68f233 100644 --- a/src/theory/quantifiers/alpha_equivalence.h +++ b/src/theory/quantifiers/alpha_equivalence.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__ALPHA_EQUIVALENCE_H -#define __CVC4__ALPHA_EQUIVALENCE_H +#ifndef CVC4__ALPHA_EQUIVALENCE_H +#define CVC4__ALPHA_EQUIVALENCE_H #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp index 08e215d72..5d1967bb4 100644 --- a/src/theory/quantifiers/anti_skolem.cpp +++ b/src/theory/quantifiers/anti_skolem.cpp @@ -2,9 +2,9 @@ /*! \file anti_skolem.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h index 162140ff1..3a7dc2da8 100644 --- a/src/theory/quantifiers/anti_skolem.h +++ b/src/theory/quantifiers/anti_skolem.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANT_ANTI_SKOLEM_H -#define __CVC4__THEORY__QUANT_ANTI_SKOLEM_H +#ifndef CVC4__THEORY__QUANT_ANTI_SKOLEM_H +#define CVC4__THEORY__QUANT_ANTI_SKOLEM_H #include <map> #include <vector> diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 2525f5d18..24e3a85b5 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -2,9 +2,9 @@ /*! \file bv_inverter.cpp ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner, Andrew Reynolds + ** Aina Niemetz, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index ad16a2ed9..746bfba9a 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__BV_INVERTER_H -#define __CVC4__BV_INVERTER_H +#ifndef CVC4__BV_INVERTER_H +#define CVC4__BV_INVERTER_H #include <map> #include <unordered_map> @@ -130,4 +130,4 @@ class BvInverter } // namespace theory } // namespace CVC4 -#endif /* __CVC4__BV_INVERTER_H */ +#endif /* CVC4__BV_INVERTER_H */ diff --git a/src/theory/quantifiers/bv_inverter_utils.cpp b/src/theory/quantifiers/bv_inverter_utils.cpp index 8ad26a422..e01af3f38 100644 --- a/src/theory/quantifiers/bv_inverter_utils.cpp +++ b/src/theory/quantifiers/bv_inverter_utils.cpp @@ -1,10 +1,10 @@ /********************* */ -/*! \file bv_inverter.cpp +/*! \file bv_inverter_utils.cpp ** \verbatim ** Top contributors (to current version): ** Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/bv_inverter_utils.h b/src/theory/quantifiers/bv_inverter_utils.h index 0fec00579..264b42ef5 100644 --- a/src/theory/quantifiers/bv_inverter_utils.h +++ b/src/theory/quantifiers/bv_inverter_utils.h @@ -1,10 +1,10 @@ /********************* */ -/*! \file bv_inverter.cpp +/*! \file bv_inverter_utils.h ** \verbatim ** Top contributors (to current version): - ** Aina Niemetz, Mathias Preiner + ** Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__BV_INVERTER_UTILS_H -#define __CVC4__BV_INVERTER_UTILS_H +#ifndef CVC4__BV_INVERTER_UTILS_H +#define CVC4__BV_INVERTER_UTILS_H #include "expr/node.h" diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp index 2d2e9ce30..e00bc957f 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.cpp +++ b/src/theory/quantifiers/candidate_rewrite_database.cpp @@ -2,9 +2,9 @@ /*! \file candidate_rewrite_database.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -69,9 +69,29 @@ void CandidateRewriteDatabase::initializeSygus(const std::vector<Node>& vars, } bool CandidateRewriteDatabase::addTerm(Node sol, + bool rec, std::ostream& out, bool& rew_print) { + // have we added this term before? + std::unordered_map<Node, bool, NodeHashFunction>::iterator itac = + d_add_term_cache.find(sol); + if (itac != d_add_term_cache.end()) + { + return itac->second; + } + + if (rec) + { + // if recursive, we first add all subterms + for (const Node& solc : sol) + { + // whether a candidate rewrite is printed for any subterm is irrelevant + bool rew_printc = false; + addTerm(solc, rec, out, rew_printc); + } + } + // register the term bool is_unique_term = true; Node eq_sol = d_sampler->registerTerm(sol); // eq_sol is a candidate solution that is equivalent to sol @@ -117,9 +137,9 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // options as the SmtEngine we belong to, where we ensure that // produce-models is set. bool needExport = false; - ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr<SmtEngine> rrChecker; + ExprManagerMapCollection varMap; initializeChecker(rrChecker, em, varMap, crr, needExport); Result r = rrChecker->checkSat(); Trace("rr-check") << "...result : " << r << std::endl; @@ -252,13 +272,18 @@ bool CandidateRewriteDatabase::addTerm(Node sol, // it discards it as a redundant candidate rewrite rule before // checking its correctness. } + d_add_term_cache[sol] = is_unique_term; return is_unique_term; } -bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) +bool CandidateRewriteDatabase::addTerm(Node sol, bool rec, std::ostream& out) { bool rew_print = false; - return addTerm(sol, out, rew_print); + return addTerm(sol, rec, out, rew_print); +} +bool CandidateRewriteDatabase::addTerm(Node sol, std::ostream& out) +{ + return addTerm(sol, false, out); } void CandidateRewriteDatabase::setSilent(bool flag) { d_silent = flag; } @@ -298,7 +323,7 @@ bool CandidateRewriteDatabaseGen::addTerm(Node n, std::ostream& out) Trace("synth-rr-dbg") << "...finish." << std::endl; } Trace("synth-rr-dbg") << "Add term " << nr << " for " << tn << std::endl; - return itc->second.addTerm(nr, out); + return itc->second.addTerm(nr, false, out); } } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 5b8ffbd94..b68b20998 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H -#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H +#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H +#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H #include <map> #include <memory> @@ -71,9 +71,13 @@ class CandidateRewriteDatabase : public ExprMiner * cause a candidate-rewrite to be printed on the output stream out. * We return true if the term sol is distinct (up to equivalence) with * all previous terms added to this class. The argument rew_print is set to - * true if this class printed a rewrite. + * true if this class printed a rewrite involving sol. + * + * If the flag rec is true, then we also recursively add all subterms of sol + * to this class as well. */ - bool addTerm(Node sol, std::ostream& out, bool& rew_print); + bool addTerm(Node sol, bool rec, std::ostream& out, bool& rew_print); + bool addTerm(Node sol, bool rec, std::ostream& out); bool addTerm(Node sol, std::ostream& out) override; /** sets whether this class should output candidate rewrites it finds */ void setSilent(bool flag); @@ -93,6 +97,8 @@ class CandidateRewriteDatabase : public ExprMiner bool d_using_sygus; /** candidate rewrite filter */ CandidateRewriteFilter d_crewrite_filter; + /** the cache for results of addTerm */ + std::unordered_map<Node, bool, NodeHashFunction> d_add_term_cache; /** if true, we silence the output of candidate rewrites */ bool d_silent; }; @@ -115,7 +121,8 @@ class CandidateRewriteDatabaseGen * This registers term n with this class. We generate the candidate rewrite * database of the appropriate type (if not allocated already), and register * n with this database. This may result in "candidate-rewrite" being - * printed on the output stream out. + * printed on the output stream out. We return true if the term sol is + * distinct (up to equivalence) with all previous terms added to this class. */ bool addTerm(Node n, std::ostream& out); @@ -138,4 +145,4 @@ class CandidateRewriteDatabaseGen } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_DATABASE_H */ diff --git a/src/theory/quantifiers/candidate_rewrite_filter.cpp b/src/theory/quantifiers/candidate_rewrite_filter.cpp index 0d3878149..53c40464f 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.cpp +++ b/src/theory/quantifiers/candidate_rewrite_filter.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -290,6 +290,12 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) // ----- check rewriting redundancy if (keep && options::sygusRewSynthFilterCong()) { + // When using sygus types, this filtering applies to the builtin versions + // of n and eq_n. This means that we may filter out a rewrite rule for one + // sygus type based on another, e.g. we won't report x=x+0 for both A and B + // in: + // A -> x | 0 | A+A + // B -> x | 0 | B+B Trace("cr-filter-debug") << "Check equal rewrite pair..." << std::endl; if (d_drewrite->areEqual(bn, beq_n)) { @@ -309,7 +315,9 @@ bool CandidateRewriteFilter::filterPair(Node n, Node eq_n) Node bni = d_drewrite->toInternal(bn); if (!bni.isNull()) { - if (!d_match_trie.getMatches(bni, &d_ssenm)) + // as with congruence filtering, we cache based on the builtin type + TypeNode tn = bn.getType(); + if (!d_match_trie[tn].getMatches(bni, &d_ssenm)) { keep = false; Trace("cr-filter") << "...redundant (matchable)" << std::endl; @@ -357,6 +365,8 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) } if (options::sygusRewSynthFilterMatch()) { + // cache based on the builtin type + TypeNode tn = bn.getType(); // add to match information for (unsigned r = 0; r < 2; r++) { @@ -369,7 +379,7 @@ void CandidateRewriteFilter::registerRelevantPair(Node n, Node eq_n) Node ti = d_drewrite->toInternal(t); if (!ti.isNull()) { - d_match_trie.addTerm(ti); + d_match_trie[tn].addTerm(ti); } } d_pairs[t].insert(to); diff --git a/src/theory/quantifiers/candidate_rewrite_filter.h b/src/theory/quantifiers/candidate_rewrite_filter.h index ca071faa4..af9ac6d87 100644 --- a/src/theory/quantifiers/candidate_rewrite_filter.h +++ b/src/theory/quantifiers/candidate_rewrite_filter.h @@ -2,9 +2,9 @@ /*! \file candidate_rewrite_filter.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H -#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H +#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H +#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H #include <map> #include "theory/quantifiers/dynamic_rewrite.h" @@ -165,14 +165,16 @@ class CandidateRewriteFilter * detail, if (t,s) is a relevant pair, then t in d_pairs[s]. */ std::map<Node, std::unordered_set<Node, NodeHashFunction> > d_pairs; - /** Match trie storing all terms in the domain of d_pairs. + /** + * For each (builtin) type, a match trie storing all terms in the domain of + * d_pairs. * * Notice that we store d_drewrite->toInternal(t) instead of t, for each * term t, so that polymorphism is handled properly. In particular, this * prevents matches between terms select( x, y ) and select( z, y ) where * the type of x and z are different. */ - MatchTrie d_match_trie; + std::map<TypeNode, MatchTrie> d_match_trie; /** Notify class */ class CandidateRewriteFilterNotifyMatch : public NotifyMatch { @@ -221,4 +223,4 @@ class CandidateRewriteFilter } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_REWRITE_FILTER_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index 4ea006d54..fa02c6d09 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -2,9 +2,9 @@ /*! \file ceg_arith_instantiator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index b6e22329d..8799ce1cd 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_arith_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H -#define __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H +#define CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H #include <vector> #include "expr/node.h" @@ -203,4 +203,4 @@ class ArithInstantiator : public Instantiator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEG_ARITH_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp index 272914c25..28a24d884 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h index 35bc6c042..466eba6a2 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_bv_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H -#define __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H +#define CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H #include <unordered_map> #include "theory/quantifiers/bv_inverter.h" @@ -211,4 +211,4 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEG_BV_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp index b74d358ac..b351dc83c 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp @@ -1,10 +1,10 @@ /********************* */ -/*! \file ceg_bv_instantiator.cpp +/*! \file ceg_bv_instantiator_utils.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** Mathias Preiner, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h index 551ce08e0..7c72a29f2 100644 --- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h +++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h @@ -1,10 +1,10 @@ /********************* */ -/*! \file ceg_bv_instantiator.cpp +/*! \file ceg_bv_instantiator_utils.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Aina Niemetz + ** Mathias Preiner, Aina Niemetz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__BV_INSTANTIATOR_UTILS_H -#define __CVC4__BV_INSTANTIATOR_UTILS_H +#ifndef CVC4__BV_INSTANTIATOR_UTILS_H +#define CVC4__BV_INSTANTIATOR_UTILS_H #include "expr/attribute.h" #include "expr/node.h" diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp index e56d5f5db..0bdcbe0d7 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp @@ -2,9 +2,9 @@ /*! \file ceg_dt_instantiator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h index 6cf3bdf42..cf9736abe 100644 --- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_dt_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H -#define __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H +#define CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H #include "expr/node.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" @@ -93,4 +93,4 @@ class DtInstantiator : public Instantiator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEG_DT_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp index df6690273..f0ea7ab7b 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp @@ -2,9 +2,9 @@ /*! \file ceg_epr_instantiator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h index f5057ad86..05932de7e 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_epr_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H -#define __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H +#define CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H #include <map> #include <vector> @@ -106,4 +106,4 @@ class EprInstantiator : public Instantiator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEG_EPR_INSTANTIATOR_H */ diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 46649154e..b11358543 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -2,9 +2,9 @@ /*! \file ceg_instantiator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h index ae191cf91..0a09f39c7 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h @@ -2,9 +2,9 @@ /*! \file ceg_instantiator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H -#define __CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H +#define CVC4__THEORY__QUANTIFIERS__CEG_INSTANTIATOR_H #include "theory/quantifiers_engine.h" #include "util/statistics_registry.h" diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 3ea3e72e4..7cfda5ba1 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -2,9 +2,9 @@ /*! \file inst_strategy_cegqi.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index 0a19727b8..ebebb808d 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -2,9 +2,9 @@ /*! \file inst_strategy_cegqi.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H -#define __CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H +#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H +#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_CEGQI_H #include "theory/decision_manager.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 7408678e7..1d9ed1639 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -2,9 +2,9 @@ /*! \file conjecture_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Dejan Jovanovic + ** Andrew Reynolds, Aina Niemetz, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 8fff7eafe..236c08138 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/dynamic_rewrite.cpp b/src/theory/quantifiers/dynamic_rewrite.cpp index f48f73aee..cd73ffe33 100644 --- a/src/theory/quantifiers/dynamic_rewrite.cpp +++ b/src/theory/quantifiers/dynamic_rewrite.cpp @@ -2,9 +2,9 @@ /*! \file dynamic_rewrite.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/dynamic_rewrite.h b/src/theory/quantifiers/dynamic_rewrite.h index 50bae0268..969b6bf93 100644 --- a/src/theory/quantifiers/dynamic_rewrite.h +++ b/src/theory/quantifiers/dynamic_rewrite.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H -#define __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H +#ifndef CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H +#define CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H #include <map> @@ -121,4 +121,4 @@ class DynamicRewriter } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__DYNAMIC_REWRITER_H */ diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 612a1938a..cb0fcaf50 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -2,9 +2,9 @@ /*! \file candidate_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/ematching/candidate_generator.h b/src/theory/quantifiers/ematching/candidate_generator.h index da4ec2d83..8cff12477 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.h +++ b/src/theory/quantifiers/ematching/candidate_generator.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H -#define __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H +#define CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H #include "theory/theory.h" #include "theory/uf/equality_engine.h" @@ -212,4 +212,4 @@ class CandidateGeneratorConsExpand : public CandidateGeneratorQE }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CANDIDATE_GENERATOR_H */ diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp index 2fcfa19d9..7598e6fdc 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.cpp +++ b/src/theory/quantifiers/ematching/ho_trigger.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -270,6 +270,11 @@ bool HigherOrderTrigger::sendInstantiation(InstMatch& m) // Assert( f==value ); for (unsigned k = 0, size = args.size(); k < size; k++) { + // must now subsitute back, to handle cases like + // (@ x y) matching (@ t (@ t s)) + // where the above substitution would produce (@ x (@ x s)), + // but the argument should be (@ t s). + args[k] = args[k].substitute(var, value); Node val = args[k]; std::map<unsigned, Node>::iterator itf = fixed_vals.find(k); if (itf == fixed_vals.end()) diff --git a/src/theory/quantifiers/ematching/ho_trigger.h b/src/theory/quantifiers/ematching/ho_trigger.h index 8840c949f..6f0ff0635 100644 --- a/src/theory/quantifiers/ematching/ho_trigger.h +++ b/src/theory/quantifiers/ematching/ho_trigger.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H -#define __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H +#ifndef CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H +#define CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H #include <map> #include <unordered_set> @@ -275,4 +275,4 @@ class HigherOrderTrigger : public Trigger } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__HO_TRIGGER_H */ diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index f26df5b79..0a4386db9 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -2,9 +2,9 @@ /*! \file inst_match_generator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index 83d4ce82e..3995c67b4 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -2,9 +2,9 @@ /*! \file inst_match_generator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Clark Barrett + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H -#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H +#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #include <map> #include "expr/node_trie.h" diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp index 6784fb8e3..8f671fb55 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp @@ -2,9 +2,9 @@ /*! \file inst_strategy_e_matching.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h index a8d53cf4b..5eb992368 100644 --- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.h +++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__INST_STRATEGY_E_MATCHING_H -#define __CVC4__INST_STRATEGY_E_MATCHING_H +#ifndef CVC4__INST_STRATEGY_E_MATCHING_H +#define CVC4__INST_STRATEGY_E_MATCHING_H #include "context/context.h" #include "context/context_mm.h" diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp index 2aa8af53d..d2650f01f 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.cpp +++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/ematching/instantiation_engine.h b/src/theory/quantifiers/ematching/instantiation_engine.h index c94320b74..139adcb04 100644 --- a/src/theory/quantifiers/ematching/instantiation_engine.h +++ b/src/theory/quantifiers/ematching/instantiation_engine.h @@ -2,9 +2,9 @@ /*! \file instantiation_engine.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H -#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H +#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H +#define CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H #include <memory> @@ -95,4 +95,4 @@ class InstantiationEngine : public QuantifiersModule { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATION_ENGINE_H */ diff --git a/src/theory/quantifiers/ematching/trigger.cpp b/src/theory/quantifiers/ematching/trigger.cpp index b50deea11..31bd1aa96 100644 --- a/src/theory/quantifiers/ematching/trigger.cpp +++ b/src/theory/quantifiers/ematching/trigger.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/ematching/trigger.h b/src/theory/quantifiers/ematching/trigger.h index bbd7c386b..f276585d6 100644 --- a/src/theory/quantifiers/ematching/trigger.h +++ b/src/theory/quantifiers/ematching/trigger.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__TRIGGER_H -#define __CVC4__THEORY__QUANTIFIERS__TRIGGER_H +#ifndef CVC4__THEORY__QUANTIFIERS__TRIGGER_H +#define CVC4__THEORY__QUANTIFIERS__TRIGGER_H #include <map> @@ -464,4 +464,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TRIGGER_H */ diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index f4a4a34a7..ef80af5f5 100644 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp @@ -2,9 +2,9 @@ /*! \file equality_infer.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tianyi Liang ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 49d208d99..69cd12a70 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -2,9 +2,9 @@ /*! \file equality_infer.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Andres Noetzli + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H -#define __CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H +#ifndef CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H +#define CVC4__THEORY__QUANTIFIERS__EQUALITY_INFER_H #include <iostream> #include <map> diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index ae560c5e5..030b0dccb 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -2,9 +2,9 @@ /*! \file equality_query.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/equality_query.h b/src/theory/quantifiers/equality_query.h index 8f836f9c6..e4eeeffa7 100644 --- a/src/theory/quantifiers/equality_query.h +++ b/src/theory/quantifiers/equality_query.h @@ -2,9 +2,9 @@ /*! \file equality_query.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H -#define __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H +#ifndef CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H +#define CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H #include "context/cdo.h" #include "context/context.h" @@ -120,4 +120,4 @@ class EqualityQueryQuantifiersEngine : public EqualityQuery }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ +#endif /* CVC4__THEORY__QUANTIFIERS_EQUALITY_QUERY_H */ diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp index b65d1c522..98d07fdea 100644 --- a/src/theory/quantifiers/expr_miner.cpp +++ b/src/theory/quantifiers/expr_miner.cpp @@ -2,9 +2,9 @@ /*! \file expr_miner.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -87,9 +87,11 @@ void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker, try { checker.reset(new SmtEngine(&em)); + checker->setIsInternalSubsolver(); checker->setTimeLimit(options::sygusExprMinerCheckTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); checker->setOption("sygus-rr-synth-input", false); + checker->setOption("sygus-abduct", false); checker->setOption("input-language", "smt2"); Expr equery = squery.toExpr().exportTo(&em, varMap); checker->assertFormula(equery); @@ -129,9 +131,9 @@ Result ExprMiner::doCheck(Node query) } NodeManager* nm = NodeManager::currentNM(); bool needExport = false; - ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr<SmtEngine> smte; + ExprManagerMapCollection varMap; initializeChecker(smte, em, varMap, queryr, needExport); return smte->checkSat(); } diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h index 59d9989c5..233ef39f7 100644 --- a/src/theory/quantifiers/expr_miner.h +++ b/src/theory/quantifiers/expr_miner.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H -#define __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H +#ifndef CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H +#define CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H #include <map> #include <memory> @@ -106,4 +106,4 @@ class ExprMiner } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__EXPRESSION_MINER_H */ diff --git a/src/theory/quantifiers/expr_miner_manager.cpp b/src/theory/quantifiers/expr_miner_manager.cpp index a808d386c..3db0e14ab 100644 --- a/src/theory/quantifiers/expr_miner_manager.cpp +++ b/src/theory/quantifiers/expr_miner_manager.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -15,6 +15,8 @@ #include "theory/quantifiers/expr_miner_manager.h" #include "theory/quantifiers_engine.h" +#include "options/quantifiers_options.h" + namespace CVC4 { namespace theory { namespace quantifiers { @@ -140,7 +142,7 @@ bool ExpressionMinerManager::addTerm(Node sol, bool ret = true; if (d_doRewSynth) { - ret = d_crd.addTerm(sol, out, rew_print); + ret = d_crd.addTerm(sol, options::sygusRewSynthRec(), out, rew_print); } // a unique term, let's try the query generator diff --git a/src/theory/quantifiers/expr_miner_manager.h b/src/theory/quantifiers/expr_miner_manager.h index d817d3775..1c8aab826 100644 --- a/src/theory/quantifiers/expr_miner_manager.h +++ b/src/theory/quantifiers/expr_miner_manager.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H -#define __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H +#ifndef CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H +#define CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H #include "expr/node.h" #include "theory/quantifiers/candidate_rewrite_database.h" @@ -120,4 +120,4 @@ class ExpressionMinerManager } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__EXPR_MINER_MANAGER_H */ diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp index 46dcb7151..0fbd971fd 100644 --- a/src/theory/quantifiers/extended_rewrite.cpp +++ b/src/theory/quantifiers/extended_rewrite.cpp @@ -2,9 +2,9 @@ /*! \file extended_rewrite.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/extended_rewrite.h b/src/theory/quantifiers/extended_rewrite.h index da77bda51..836e15b7b 100644 --- a/src/theory/quantifiers/extended_rewrite.h +++ b/src/theory/quantifiers/extended_rewrite.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H -#define __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H +#ifndef CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H +#define CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H #include <unordered_map> @@ -250,4 +250,4 @@ class ExtendedRewriter } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */ diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index 5eb65ed21..5428d9f1a 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -2,9 +2,9 @@ /*! \file first_order_model.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h index b96b42dc2..bdf1d7c15 100644 --- a/src/theory/quantifiers/first_order_model.h +++ b/src/theory/quantifiers/first_order_model.h @@ -2,9 +2,9 @@ /*! \file first_order_model.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Paul Meng + ** Andrew Reynolds, Paul Meng, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__FIRST_ORDER_MODEL_H -#define __CVC4__FIRST_ORDER_MODEL_H +#ifndef CVC4__FIRST_ORDER_MODEL_H +#define CVC4__FIRST_ORDER_MODEL_H #include "theory/theory_model.h" #include "theory/uf/theory_uf_model.h" @@ -218,4 +218,4 @@ class FirstOrderModelFmc : public FirstOrderModel }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__FIRST_ORDER_MODEL_H */ +#endif /* CVC4__FIRST_ORDER_MODEL_H */ diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index cafa4a749..e15fc85bb 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -2,9 +2,9 @@ /*! \file bounded_integers.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Tim King + ** Andrew Reynolds, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index b3132a4a7..55ed5bdd2 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__BOUNDED_INTEGERS_H -#define __CVC4__BOUNDED_INTEGERS_H +#ifndef CVC4__BOUNDED_INTEGERS_H +#define CVC4__BOUNDED_INTEGERS_H #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp index 481048105..ace5c2b26 100644 --- a/src/theory/quantifiers/fmf/full_model_check.cpp +++ b/src/theory/quantifiers/fmf/full_model_check.cpp @@ -2,9 +2,9 @@ /*! \file full_model_check.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Kshitij Bansal + ** Andrew Reynolds, Morgan Deters, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/fmf/full_model_check.h b/src/theory/quantifiers/fmf/full_model_check.h index f0f9a1798..7dd1991f5 100644 --- a/src/theory/quantifiers/fmf/full_model_check.h +++ b/src/theory/quantifiers/fmf/full_model_check.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H -#define __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H +#ifndef CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H +#define CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H #include "theory/quantifiers/fmf/model_builder.h" #include "theory/quantifiers/first_order_model.h" @@ -162,4 +162,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__FULL_MODEL_CHECK_H */ diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp index 8ef30fc4d..51cd8481f 100644 --- a/src/theory/quantifiers/fmf/model_builder.cpp +++ b/src/theory/quantifiers/fmf/model_builder.cpp @@ -2,9 +2,9 @@ /*! \file model_builder.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/fmf/model_builder.h b/src/theory/quantifiers/fmf/model_builder.h index b73716169..1b4d24779 100644 --- a/src/theory/quantifiers/fmf/model_builder.h +++ b/src/theory/quantifiers/fmf/model_builder.h @@ -2,9 +2,9 @@ /*! \file model_builder.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H -#define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H +#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H +#define CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H #include "theory/quantifiers_engine.h" #include "theory/theory_model_builder.h" @@ -60,4 +60,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H */ diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index d2579b4ee..5609cade6 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -266,7 +266,8 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ } d_triedLemmas += mb->getNumTriedLemmas()-prev_tlem; d_addedLemmas += mb->getNumAddedLemmas()-prev_alem; - d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += mb->getNumAddedLemmas(); + d_quantEngine->d_statistics.d_instantiations_fmf_mbqi += + (mb->getNumAddedLemmas() - prev_alem); }else{ if( Trace.isOn("fmf-exh-inst-debug") ){ Trace("fmf-exh-inst-debug") << " Instantiation Constants: "; diff --git a/src/theory/quantifiers/fmf/model_engine.h b/src/theory/quantifiers/fmf/model_engine.h index a11115f33..41bc312e7 100644 --- a/src/theory/quantifiers/fmf/model_engine.h +++ b/src/theory/quantifiers/fmf/model_engine.h @@ -2,9 +2,9 @@ /*! \file model_engine.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H -#define __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H +#ifndef CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H +#define CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H #include "theory/quantifiers_engine.h" #include "theory/quantifiers/fmf/model_builder.h" @@ -67,4 +67,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__MODEL_ENGINE_H */ diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 1671fa1a0..185a349c0 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -2,9 +2,9 @@ /*! \file fun_def_process.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h index 78adc710c..0282f0e40 100644 --- a/src/theory/quantifiers/fun_def_process.h +++ b/src/theory/quantifiers/fun_def_process.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H -#define __CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H +#ifndef CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H +#define CVC4__QUANTIFIERS_FUN_DEF_PROCESS_H #include <iostream> #include <string> diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp index a16e03420..069d5b888 100644 --- a/src/theory/quantifiers/inst_match.cpp +++ b/src/theory/quantifiers/inst_match.cpp @@ -2,9 +2,9 @@ /*! \file inst_match.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Morgan Deters, Clark Barrett + ** Andrew Reynolds, Morgan Deters, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h index 5695d1294..d298c43a8 100644 --- a/src/theory/quantifiers/inst_match.h +++ b/src/theory/quantifiers/inst_match.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H -#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H +#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_H +#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_H #include <vector> @@ -102,4 +102,4 @@ typedef CVC4::theory::inst::InstMatch InstMatch; }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ diff --git a/src/theory/quantifiers/inst_match_trie.cpp b/src/theory/quantifiers/inst_match_trie.cpp index aba4a3b5e..8b8689835 100644 --- a/src/theory/quantifiers/inst_match_trie.cpp +++ b/src/theory/quantifiers/inst_match_trie.cpp @@ -2,9 +2,9 @@ /*! \file inst_match_trie.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/inst_match_trie.h b/src/theory/quantifiers/inst_match_trie.h index 50df50786..4854616db 100644 --- a/src/theory/quantifiers/inst_match_trie.h +++ b/src/theory/quantifiers/inst_match_trie.h @@ -2,9 +2,9 @@ /*! \file inst_match_trie.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H -#define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H +#ifndef CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H +#define CVC4__THEORY__QUANTIFIERS__INST_MATCH_TRIE_H #include <map> @@ -436,4 +436,4 @@ class InstMatchTrieOrdered } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INST_MATCH_H */ diff --git a/src/theory/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp index 15dd35c26..56be1506c 100644 --- a/src/theory/quantifiers/inst_propagator.cpp +++ b/src/theory/quantifiers/inst_propagator.cpp @@ -2,9 +2,9 @@ /*! \file inst_propagator.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index 1ba359228..d45b078ce 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -2,9 +2,9 @@ /*! \file inst_propagator.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__QUANTIFIERS_INST_PROPAGATOR_H -#define __CVC4__QUANTIFIERS_INST_PROPAGATOR_H +#ifndef CVC4__QUANTIFIERS_INST_PROPAGATOR_H +#define CVC4__QUANTIFIERS_INST_PROPAGATOR_H #include <iostream> #include <map> diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp index 9d70d0d4b..7a2f62864 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.cpp +++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp @@ -2,9 +2,9 @@ /*! \file inst_strategy_enumerative.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -70,46 +70,89 @@ void InstStrategyEnum::check(Theory::Effort e, QEffort quant_e) doCheck = quant_e == QEFFORT_LAST_CALL; fullEffort = !d_quantEngine->hasAddedLemma(); } - if (doCheck) + if (!doCheck) { - double clSet = 0; - if (Trace.isOn("fs-engine")) - { - clSet = double(clock()) / double(CLOCKS_PER_SEC); - Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" - << std::endl; - } - int addedLemmas = 0; - for (unsigned i = 0; - i < d_quantEngine->getModel()->getNumAssertedQuantifiers(); - i++) + return; + } + double clSet = 0; + if (Trace.isOn("fs-engine")) + { + clSet = double(clock()) / double(CLOCKS_PER_SEC); + Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" + << std::endl; + } + unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; + unsigned rend = fullEffort ? 1 : rstart; + unsigned addedLemmas = 0; + // First try in relevant domain of all quantified formulas, if no + // instantiations exist, try arbitrary ground terms. + // Notice that this stratification of effort levels makes it so that some + // quantified formulas may not be instantiated (if they have no instances + // at effort level r=0 but another quantified formula does). We prefer + // this stratification since effort level r=1 may be highly expensive in the + // case where we have a quantified formula with many entailed instances. + FirstOrderModel* fm = d_quantEngine->getModel(); + RelevantDomain* rd = d_quantEngine->getRelevantDomain(); + unsigned nquant = fm->getNumAssertedQuantifiers(); + std::map<Node, bool> alreadyProc; + for (unsigned r = rstart; r <= rend; r++) + { + if (rd || r > 0) { - Node q = d_quantEngine->getModel()->getAssertedQuantifier(i, true); - if (d_quantEngine->hasOwnership(q, this) - && d_quantEngine->getModel()->isQuantifierActive(q)) + if (r == 0) + { + Trace("inst-alg") << "-> Relevant domain instantiate..." << std::endl; + Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; + rd->compute(); + Trace("inst-alg-debug") << "...finished" << std::endl; + } + else + { + Trace("inst-alg") << "-> Ground term instantiate..." << std::endl; + } + for (unsigned i = 0; i < nquant; i++) { - if (process(q, fullEffort)) + Node q = fm->getAssertedQuantifier(i, true); + bool doProcess = d_quantEngine->hasOwnership(q, this) + && fm->isQuantifierActive(q) + && alreadyProc.find(q) == alreadyProc.end(); + if (doProcess) { - // added lemma - addedLemmas++; - if (d_quantEngine->inConflict()) + if (process(q, fullEffort, r == 0)) { - break; + // don't need to mark this if we are not stratifying + if (!options::fullSaturateStratify()) + { + alreadyProc[q] = true; + } + // added lemma + addedLemmas++; + if (d_quantEngine->inConflict()) + { + break; + } } } } + if (d_quantEngine->inConflict() + || (addedLemmas > 0 && options::fullSaturateStratify())) + { + // we break if we are in conflict, or if we added any lemma at this + // effort level and we stratify effort levels. + break; + } } - if (Trace.isOn("fs-engine")) - { - Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; - double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); - Trace("fs-engine") << "Finished full saturation engine, time = " - << (clSet2 - clSet) << std::endl; - } + } + if (Trace.isOn("fs-engine")) + { + Trace("fs-engine") << "Added lemmas = " << addedLemmas << std::endl; + double clSet2 = double(clock()) / double(CLOCKS_PER_SEC); + Trace("fs-engine") << "Finished full saturation engine, time = " + << (clSet2 - clSet) << std::endl; } } -bool InstStrategyEnum::process(Node f, bool fullEffort) +bool InstStrategyEnum::process(Node f, bool fullEffort, bool isRd) { // ignore if constant true (rare case of non-standard quantifier whose body is // rewritten to true) @@ -117,178 +160,156 @@ bool InstStrategyEnum::process(Node f, bool fullEffort) { return false; } - // first, try from relevant domain RelevantDomain* rd = d_quantEngine->getRelevantDomain(); - unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1; - unsigned rend = fullEffort ? 1 : rstart; - for (unsigned r = rstart; r <= rend; r++) + unsigned final_max_i = 0; + std::vector<unsigned> maxs; + std::vector<bool> max_zero; + bool has_zero = false; + std::map<TypeNode, std::vector<Node> > term_db_list; + std::vector<TypeNode> ftypes; + TermDb* tdb = d_quantEngine->getTermDatabase(); + EqualityQuery* qy = d_quantEngine->getEqualityQuery(); + // iterate over substitutions for variables + for (unsigned i = 0; i < f[0].getNumChildren(); i++) { - if (rd || r > 0) + TypeNode tn = f[0][i].getType(); + ftypes.push_back(tn); + unsigned ts; + if (isRd) { - if (r == 0) + ts = rd->getRDomain(f, i)->d_terms.size(); + } + else + { + ts = tdb->getNumTypeGroundTerms(tn); + std::map<TypeNode, std::vector<Node> >::iterator ittd = + term_db_list.find(tn); + if (ittd == term_db_list.end()) { - Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." - << std::endl; - Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl; - rd->compute(); - Trace("inst-alg-debug") << "...finished" << std::endl; + std::map<Node, Node> reps_found; + for (unsigned j = 0; j < ts; j++) + { + Node gt = tdb->getTypeGroundTerm(ftypes[i], j); + if (!options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(gt)) + { + Node rep = qy->getRepresentative(gt); + if (reps_found.find(rep) == reps_found.end()) + { + reps_found[rep] = gt; + term_db_list[tn].push_back(gt); + } + } + } + ts = term_db_list[tn].size(); } else { - Trace("inst-alg") << "-> Ground term instantiate " << f << "..." - << std::endl; + ts = ittd->second.size(); } - unsigned final_max_i = 0; - std::vector<unsigned> maxs; - std::vector<bool> max_zero; - bool has_zero = false; - std::map<TypeNode, std::vector<Node> > term_db_list; - std::vector<TypeNode> ftypes; - // iterate over substitutions for variables - for (unsigned i = 0; i < f[0].getNumChildren(); i++) + } + // consider a default value if at full effort + max_zero.push_back(fullEffort && ts == 0); + ts = (fullEffort && ts == 0) ? 1 : ts; + Trace("inst-alg-rd") << "Variable " << i << " has " << ts + << " in relevant domain." << std::endl; + if (ts == 0) + { + has_zero = true; + break; + } + maxs.push_back(ts); + if (ts > final_max_i) + { + final_max_i = ts; + } + } + if (!has_zero) + { + Trace("inst-alg-rd") << "Will do " << final_max_i + << " stages of instantiation." << std::endl; + unsigned max_i = 0; + bool success; + Instantiate* ie = d_quantEngine->getInstantiate(); + while (max_i <= final_max_i) + { + Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; + std::vector<unsigned> childIndex; + int index = 0; + do { - TypeNode tn = f[0][i].getType(); - ftypes.push_back(tn); - unsigned ts; - if (r == 0) - { - ts = rd->getRDomain(f, i)->d_terms.size(); - } - else + while (index >= 0 && index < (int)f[0].getNumChildren()) { - ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms(tn); - std::map<TypeNode, std::vector<Node> >::iterator ittd = - term_db_list.find(tn); - if (ittd == term_db_list.end()) + if (index == static_cast<int>(childIndex.size())) { - std::map<Node, Node> reps_found; - for (unsigned j = 0; j < ts; j++) - { - Node gt = d_quantEngine->getTermDatabase()->getTypeGroundTerm( - ftypes[i], j); - if (!options::cbqi() - || !quantifiers::TermUtil::hasInstConstAttr(gt)) - { - Node rep = - d_quantEngine->getEqualityQuery()->getRepresentative(gt); - if (reps_found.find(rep) == reps_found.end()) - { - reps_found[rep] = gt; - term_db_list[tn].push_back(gt); - } - } - } - ts = term_db_list[tn].size(); + childIndex.push_back(-1); } else { - ts = ittd->second.size(); + Assert(index == static_cast<int>(childIndex.size()) - 1); + unsigned nv = childIndex[index] + 1; + if (nv < maxs[index] && nv <= max_i) + { + childIndex[index] = nv; + index++; + } + else + { + childIndex.pop_back(); + index--; + } } } - // consider a default value if at full effort - max_zero.push_back(fullEffort && ts == 0); - ts = (fullEffort && ts == 0) ? 1 : ts; - Trace("inst-alg-rd") << "Variable " << i << " has " << ts - << " in relevant domain." << std::endl; - if (ts == 0) + success = index >= 0; + if (success) { - has_zero = true; - break; - } - else - { - maxs.push_back(ts); - if (ts > final_max_i) + if (Trace.isOn("inst-alg-rd")) { - final_max_i = ts; + Trace("inst-alg-rd") << "Try instantiation { "; + for (unsigned i : childIndex) + { + Trace("inst-alg-rd") << i << " "; + } + Trace("inst-alg-rd") << "}" << std::endl; } - } - } - if (!has_zero) - { - Trace("inst-alg-rd") << "Will do " << final_max_i - << " stages of instantiation." << std::endl; - unsigned max_i = 0; - bool success; - while (max_i <= final_max_i) - { - Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl; - std::vector<unsigned> childIndex; - int index = 0; - do + // try instantiation + std::vector<Node> terms; + for (unsigned i = 0, nchild = f[0].getNumChildren(); i < nchild; i++) { - while (index >= 0 && index < (int)f[0].getNumChildren()) + if (max_zero[i]) { - if (index == (int)childIndex.size()) - { - childIndex.push_back(-1); - } - else - { - Assert(index == (int)(childIndex.size()) - 1); - unsigned nv = childIndex[index] + 1; - if (nv < maxs[index] && nv <= max_i) - { - childIndex[index] = nv; - index++; - } - else - { - childIndex.pop_back(); - index--; - } - } + // no terms available, will report incomplete instantiation + terms.push_back(Node::null()); + Trace("inst-alg-rd") << " null" << std::endl; } - success = index >= 0; - if (success) + else if (isRd) { - Trace("inst-alg-rd") << "Try instantiation { "; - for (unsigned j = 0; j < childIndex.size(); j++) - { - Trace("inst-alg-rd") << childIndex[j] << " "; - } - Trace("inst-alg-rd") << "}" << std::endl; - // try instantiation - std::vector<Node> terms; - for (unsigned i = 0; i < f[0].getNumChildren(); i++) - { - if (max_zero[i]) - { - // no terms available, will report incomplete instantiation - terms.push_back(Node::null()); - Trace("inst-alg-rd") << " null" << std::endl; - } - else if (r == 0) - { - terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]); - Trace("inst-alg-rd") - << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]] - << std::endl; - } - else - { - Assert(childIndex[i] < term_db_list[ftypes[i]].size()); - terms.push_back(term_db_list[ftypes[i]][childIndex[i]]); - Trace("inst-alg-rd") << " " - << term_db_list[ftypes[i]][childIndex[i]] - << std::endl; - } - } - if (d_quantEngine->getInstantiate()->addInstantiation(f, terms)) - { - Trace("inst-alg-rd") << "Success!" << std::endl; - ++(d_quantEngine->d_statistics.d_instantiations_guess); - return true; - } - else - { - index--; - } + terms.push_back(rd->getRDomain(f, i)->d_terms[childIndex[i]]); + Trace("inst-alg-rd") + << " " << rd->getRDomain(f, i)->d_terms[childIndex[i]] + << std::endl; } - } while (success); - max_i++; + else + { + Assert(childIndex[i] < term_db_list[ftypes[i]].size()); + terms.push_back(term_db_list[ftypes[i]][childIndex[i]]); + Trace("inst-alg-rd") + << " " << term_db_list[ftypes[i]][childIndex[i]] + << std::endl; + } + } + if (ie->addInstantiation(f, terms)) + { + Trace("inst-alg-rd") << "Success!" << std::endl; + ++(d_quantEngine->d_statistics.d_instantiations_guess); + return true; + } + else + { + index--; + } } - } + } while (success); + max_i++; } } // TODO : term enumerator instantiation? diff --git a/src/theory/quantifiers/inst_strategy_enumerative.h b/src/theory/quantifiers/inst_strategy_enumerative.h index be0f452e4..920e643bc 100644 --- a/src/theory/quantifiers/inst_strategy_enumerative.h +++ b/src/theory/quantifiers/inst_strategy_enumerative.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__INST_STRATEGY_ENUMERATIVE_H -#define __CVC4__INST_STRATEGY_ENUMERATIVE_H +#ifndef CVC4__INST_STRATEGY_ENUMERATIVE_H +#define CVC4__INST_STRATEGY_ENUMERATIVE_H #include "context/context.h" #include "context/context_mm.h" @@ -92,8 +92,12 @@ class InstStrategyEnum : public QuantifiersModule * well-typed term *not* occurring in the current context. * This handles corner cases where there are no well-typed * ground terms in the current context to instantiate with. + * + * The flag isRd indicates whether we are trying relevant domain + * instantiations. If this flag is false, we are trying arbitrary ground + * term instantiations. */ - bool process(Node q, bool fullEffort); + bool process(Node q, bool fullEffort, bool isRd); }; /* class InstStrategyEnum */ } /* CVC4::theory::quantifiers namespace */ diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp index 96a28cde6..623db032a 100644 --- a/src/theory/quantifiers/instantiate.cpp +++ b/src/theory/quantifiers/instantiate.cpp @@ -2,9 +2,9 @@ /*! \file instantiate.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h index 62e0ddb55..2fdb494e9 100644 --- a/src/theory/quantifiers/instantiate.h +++ b/src/theory/quantifiers/instantiate.h @@ -2,9 +2,9 @@ /*! \file instantiate.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H -#define __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H +#ifndef CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H +#define CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H #include <map> @@ -374,4 +374,4 @@ class Instantiate : public QuantifiersUtil } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__INSTANTIATE_H */ diff --git a/src/theory/quantifiers/lazy_trie.cpp b/src/theory/quantifiers/lazy_trie.cpp index 35049b8ba..a50352df5 100644 --- a/src/theory/quantifiers/lazy_trie.cpp +++ b/src/theory/quantifiers/lazy_trie.cpp @@ -2,9 +2,9 @@ /*! \file lazy_trie.cpp ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/lazy_trie.h b/src/theory/quantifiers/lazy_trie.h index 156f1abde..8f822fcc0 100644 --- a/src/theory/quantifiers/lazy_trie.h +++ b/src/theory/quantifiers/lazy_trie.h @@ -2,9 +2,9 @@ /*! \file lazy_trie.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa + ** Haniel Barbosa, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -12,8 +12,8 @@ ** \brief lazy trie **/ -#ifndef __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H -#define __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H +#ifndef CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H +#define CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H #include "expr/node.h" @@ -170,4 +170,4 @@ class LazyTrieMulti } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__LAZY_TRIE_H */ diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index 752d61489..520088328 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -2,9 +2,9 @@ /*! \file local_theory_ext.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng + ** Andrew Reynolds, Morgan Deters, Paul Meng ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index b8b0e34fa..9793ea0a7 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H -#define __CVC4__THEORY__LOCAL_THEORY_EXT_H +#ifndef CVC4__THEORY__LOCAL_THEORY_EXT_H +#define CVC4__THEORY__LOCAL_THEORY_EXT_H #include "context/cdo.h" #include "expr/node_trie.h" diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 5b57af14c..dc18a2005 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2,9 +2,9 @@ /*! \file quant_conflict_find.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Morgan Deters + ** Andrew Reynolds, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -583,7 +583,9 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node }else{ Node inst = p->d_quantEngine->getInstantiate()->getInstantiation(d_q, terms); - Node inst_eval = p->getTermDatabase()->evaluateTerm( inst, NULL, options::qcfTConstraint() ); + inst = Rewriter::rewrite(inst); + Node inst_eval = p->getTermDatabase()->evaluateTerm( + inst, nullptr, options::qcfTConstraint(), true); if( Trace.isOn("qcf-instance-check") ){ Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl; for( unsigned i=0; i<terms.size(); i++ ){ @@ -591,10 +593,13 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node } Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl; } - if( inst_eval.isNull() || inst_eval==p->getTermUtil()->d_true || !isPropagatingInstance( p, inst_eval ) ){ + if (inst_eval.isNull() + || (inst_eval.isConst() && inst_eval.getConst<bool>())) + { Trace("qcf-instance-check") << "...spurious." << std::endl; return true; }else{ + Assert(p->isPropagatingInstance(inst_eval)); Trace("qcf-instance-check") << "...not spurious." << std::endl; } } @@ -615,27 +620,6 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node return p->d_quantEngine->inConflict(); } -bool QuantInfo::isPropagatingInstance( QuantConflictFind * p, Node n ) { - if( n.getKind()==FORALL ){ - //TODO? - return true; - }else if( n.getKind()==NOT || n.getKind()==AND || n.getKind()==OR || n.getKind()==EQUAL || n.getKind()==ITE || - ( n.getKind()==EQUAL && n[0].getType().isBoolean() ) ){ - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - if( !isPropagatingInstance( p, n[i] ) ){ - return false; - } - } - return true; - }else{ - if( p->getEqualityEngine()->hasTerm( n ) || isGroundSubterm( n ) ){ - return true; - } - } - Trace("qcf-instance-check-debug") << "...not propagating instance because of " << n << std::endl; - return false; -} - bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl; Node rew = Rewriter::rewrite( lit ); @@ -1047,7 +1031,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) else { d_qni_gterm[i] = d_n[i]; - qi->setGroundSubterm(d_n[i]); } } d_type = d_n.getKind() == EQUAL ? typ_eq : typ_tconstraint; @@ -1058,7 +1041,6 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ) //we will just evaluate d_n = n; d_type = typ_ground; - qi->setGroundSubterm( d_n ); } } Trace("qcf-qregister-debug") << "Done make match gen " << n << ", type = "; @@ -2211,6 +2193,42 @@ std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e) { return os; } +bool QuantConflictFind::isPropagatingInstance(Node n) const +{ + std::unordered_set<TNode, TNodeHashFunction> visited; + std::vector<TNode> visit; + TNode cur; + visit.push_back(n); + do + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + Kind ck = cur.getKind(); + if (ck == FORALL) + { + // do nothing + } + else if (TermUtil::isBoolConnective(ck)) + { + for (TNode cc : cur) + { + visit.push_back(cc); + } + } + else if (!getEqualityEngine()->hasTerm(cur)) + { + Trace("qcf-instance-check-debug") + << "...not propagating instance because of " << n << std::endl; + return false; + } + } + } while (!visit.empty()); + return true; +} + } /* namespace CVC4::theory::quantifiers */ } /* namespace CVC4::theory */ } /* namespace CVC4 */ diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 9fa37a96c..f22910191 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -2,9 +2,9 @@ /*! \file quant_conflict_find.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -126,13 +126,9 @@ private: //for completing match void getPropagateVars( QuantConflictFind * p, std::vector< TNode >& vars, TNode n, bool pol, std::map< TNode, bool >& visited ); //optimization: number of variables set, to track when we can stop std::map< int, bool > d_vars_set; - std::map< Node, bool > d_ground_terms; std::vector< Node > d_extra_var; public: - void setGroundSubterm( Node t ) { d_ground_terms[t] = true; } - bool isGroundSubterm( Node t ) { return d_ground_terms.find( t )!=d_ground_terms.end(); } bool isBaseMatchComplete(); - bool isPropagatingInstance( QuantConflictFind * p, Node n ); public: QuantInfo(); ~QuantInfo(); @@ -272,6 +268,22 @@ public: Statistics d_statistics; /** Identify this module */ std::string identify() const override { return "QcfEngine"; } + /** is n a propagating instance? + * + * A propagating instance is any formula that consists of Boolean connectives, + * equality, quantified formulas, and terms that exist in the current + * context (those in the master equality engine). + * + * Notice the distinction that quantified formulas that do not appear in the + * current context are considered to be legal in propagating instances. This + * choice is significant for TPTP, where a net of ~200 benchmarks are gained + * due to this decision. + * + * Propagating instances are the second most useful kind of instantiation + * after conflicting instances and are used as a second effort in the + * algorithm performed by this class. + */ + bool isPropagatingInstance(Node n) const; }; std::ostream& operator<<(std::ostream& os, const QuantConflictFind::Effort& e); diff --git a/src/theory/quantifiers/quant_epr.cpp b/src/theory/quantifiers/quant_epr.cpp index eedea6767..e03a2c120 100644 --- a/src/theory/quantifiers/quant_epr.cpp +++ b/src/theory/quantifiers/quant_epr.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/quant_epr.h b/src/theory/quantifiers/quant_epr.h index 07569a09b..1284dde33 100644 --- a/src/theory/quantifiers/quant_epr.h +++ b/src/theory/quantifiers/quant_epr.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANT_EPR_H -#define __CVC4__THEORY__QUANT_EPR_H +#ifndef CVC4__THEORY__QUANT_EPR_H +#define CVC4__THEORY__QUANT_EPR_H #include <map> @@ -101,4 +101,4 @@ class QuantEPR } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANT_EPR_H */ +#endif /* CVC4__THEORY__QUANT_EPR_H */ diff --git a/src/theory/quantifiers/quant_relevance.cpp b/src/theory/quantifiers/quant_relevance.cpp index a05388d17..de54fa05f 100644 --- a/src/theory/quantifiers/quant_relevance.cpp +++ b/src/theory/quantifiers/quant_relevance.cpp @@ -2,9 +2,9 @@ /*! \file quant_relevance.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/quant_relevance.h b/src/theory/quantifiers/quant_relevance.h index 21017e783..26a4630cd 100644 --- a/src/theory/quantifiers/quant_relevance.h +++ b/src/theory/quantifiers/quant_relevance.h @@ -2,9 +2,9 @@ /*! \file quant_relevance.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANT_RELEVANCE_H -#define __CVC4__THEORY__QUANT_RELEVANCE_H +#ifndef CVC4__THEORY__QUANT_RELEVANCE_H +#define CVC4__THEORY__QUANT_RELEVANCE_H #include <map> @@ -68,4 +68,4 @@ class QuantRelevance : public QuantifiersUtil } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANT_RELEVANCE_H */ +#endif /* CVC4__THEORY__QUANT_RELEVANCE_H */ diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index fb5492eb3..808c6006f 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -2,9 +2,9 @@ /*! \file quant_split.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h index 6a752fe3f..1a2aaa6cf 100644 --- a/src/theory/quantifiers/quant_split.h +++ b/src/theory/quantifiers/quant_split.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANT_SPLIT_H -#define __CVC4__THEORY__QUANT_SPLIT_H +#ifndef CVC4__THEORY__QUANT_SPLIT_H +#define CVC4__THEORY__QUANT_SPLIT_H #include "theory/quantifiers_engine.h" #include "context/cdo.h" diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index b1b34fb98..01f362d25 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -2,9 +2,9 @@ /*! \file quant_util.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -30,27 +30,38 @@ QuantifiersModule::QEffort QuantifiersModule::needsModel(Theory::Effort e) return QEFFORT_NONE; } -eq::EqualityEngine * QuantifiersModule::getEqualityEngine() { +eq::EqualityEngine* QuantifiersModule::getEqualityEngine() const +{ return d_quantEngine->getActiveEqualityEngine(); } -bool QuantifiersModule::areEqual( TNode n1, TNode n2 ) { +bool QuantifiersModule::areEqual(TNode n1, TNode n2) const +{ return d_quantEngine->getEqualityQuery()->areEqual( n1, n2 ); } -bool QuantifiersModule::areDisequal( TNode n1, TNode n2 ) { +bool QuantifiersModule::areDisequal(TNode n1, TNode n2) const +{ return d_quantEngine->getEqualityQuery()->areDisequal( n1, n2 ); } -TNode QuantifiersModule::getRepresentative( TNode n ) { +TNode QuantifiersModule::getRepresentative(TNode n) const +{ return d_quantEngine->getEqualityQuery()->getRepresentative( n ); } -quantifiers::TermDb * QuantifiersModule::getTermDatabase() { +QuantifiersEngine* QuantifiersModule::getQuantifiersEngine() const +{ + return d_quantEngine; +} + +quantifiers::TermDb* QuantifiersModule::getTermDatabase() const +{ return d_quantEngine->getTermDatabase(); } -quantifiers::TermUtil * QuantifiersModule::getTermUtil() { +quantifiers::TermUtil* QuantifiersModule::getTermUtil() const +{ return d_quantEngine->getTermUtil(); } diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h index e324bc36f..43861d6e9 100644 --- a/src/theory/quantifiers/quant_util.h +++ b/src/theory/quantifiers/quant_util.h @@ -2,9 +2,9 @@ /*! \file quant_util.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANT_UTIL_H -#define __CVC4__THEORY__QUANT_UTIL_H +#ifndef CVC4__THEORY__QUANT_UTIL_H +#define CVC4__THEORY__QUANT_UTIL_H #include <iostream> #include <map> @@ -138,19 +138,19 @@ class QuantifiersModule { virtual std::string identify() const = 0; //----------------------------general queries /** get currently used the equality engine */ - eq::EqualityEngine * getEqualityEngine(); + eq::EqualityEngine* getEqualityEngine() const; /** are n1 and n2 equal in the current used equality engine? */ - bool areEqual( TNode n1, TNode n2 ); + bool areEqual(TNode n1, TNode n2) const; /** are n1 and n2 disequal in the current used equality engine? */ - bool areDisequal(TNode n1, TNode n2); + bool areDisequal(TNode n1, TNode n2) const; /** get the representative of n in the current used equality engine */ - TNode getRepresentative( TNode n ); + TNode getRepresentative(TNode n) const; /** get quantifiers engine that owns this module */ - QuantifiersEngine* getQuantifiersEngine() { return d_quantEngine; } + QuantifiersEngine* getQuantifiersEngine() const; /** get currently used term database */ - quantifiers::TermDb * getTermDatabase(); + quantifiers::TermDb* getTermDatabase() const; /** get currently used term utility object */ - quantifiers::TermUtil * getTermUtil(); + quantifiers::TermUtil* getTermUtil() const; //----------------------------end general queries protected: /** pointer to the quantifiers engine that owns this module */ @@ -237,4 +237,4 @@ public: } } -#endif /* __CVC4__THEORY__QUANT_UTIL_H */ +#endif /* CVC4__THEORY__QUANT_UTIL_H */ diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index e3463df0d..d93de6a54 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -2,9 +2,9 @@ /*! \file quantifiers_attributes.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Tim King + ** Andrew Reynolds, Paul Meng, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index d3acc9434..329f9d08a 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H -#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H +#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H +#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_ATTRIBUTES_H #include "expr/attribute.h" #include "expr/node.h" diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index e2a26f6e6..015bf9c5a 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index a1d6d25c3..09f26b65b 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H -#define __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H +#define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H #include "theory/rewriter.h" #include "theory/quantifiers_engine.h" @@ -188,6 +188,6 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */ diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp index e62f3513c..bc7538c1f 100644 --- a/src/theory/quantifiers/query_generator.cpp +++ b/src/theory/quantifiers/query_generator.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -185,9 +185,9 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex) NodeManager* nm = NodeManager::currentNM(); // make the satisfiability query bool needExport = false; - ExprManagerMapCollection varMap; ExprManager em(nm->getOptions()); std::unique_ptr<SmtEngine> queryChecker; + ExprManagerMapCollection varMap; initializeChecker(queryChecker, em, varMap, qy, needExport); Result r = queryChecker->checkSat(); Trace("sygus-qgen-check") << " query: ...got : " << r << std::endl; diff --git a/src/theory/quantifiers/query_generator.h b/src/theory/quantifiers/query_generator.h index f0b3fa565..749c78c85 100644 --- a/src/theory/quantifiers/query_generator.h +++ b/src/theory/quantifiers/query_generator.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H -#define __CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H +#define CVC4__THEORY__QUANTIFIERS__QUERY_GENERATOR_H #include <map> #include <unordered_set> @@ -113,4 +113,4 @@ class QueryGenerator : public ExprMiner } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS___H */ +#endif /* CVC4__THEORY__QUANTIFIERS___H */ diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 849e73822..071bd7933 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -2,9 +2,9 @@ /*! \file relevant_domain.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -169,7 +169,9 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po computeRelevantDomainOpCh( rf, n[i] ); } } - if( n[i].getKind()!=FORALL ){ + // do not recurse under nested closures + if (!n[i].isClosure()) + { bool newHasPol; bool newPol; QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol ); diff --git a/src/theory/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h index 78fe23890..8f348b471 100644 --- a/src/theory/quantifiers/relevant_domain.h +++ b/src/theory/quantifiers/relevant_domain.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H -#define __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H +#ifndef CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H +#define CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H #include "theory/quantifiers/first_order_model.h" #include "theory/quantifiers/quant_util.h" @@ -163,4 +163,4 @@ class RelevantDomain : public QuantifiersUtil }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__RELEVANT_DOMAIN_H */ diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index ed9666d80..ff42a9c89 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -2,9 +2,9 @@ /*! \file rewrite_engine.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h index febcc0126..bbd6a1534 100644 --- a/src/theory/quantifiers/rewrite_engine.h +++ b/src/theory/quantifiers/rewrite_engine.h @@ -2,9 +2,9 @@ /*! \file rewrite_engine.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King + ** Andrew Reynolds, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__REWRITE_ENGINE_H -#define __CVC4__REWRITE_ENGINE_H +#ifndef CVC4__REWRITE_ENGINE_H +#define CVC4__REWRITE_ENGINE_H #include "context/context.h" #include "context/context_mm.h" diff --git a/src/theory/quantifiers/single_inv_partition.cpp b/src/theory/quantifiers/single_inv_partition.cpp index 851204a84..153ab71cc 100644 --- a/src/theory/quantifiers/single_inv_partition.cpp +++ b/src/theory/quantifiers/single_inv_partition.cpp @@ -2,9 +2,9 @@ /*! \file single_inv_partition.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/single_inv_partition.h b/src/theory/quantifiers/single_inv_partition.h index 199ab29d4..0a4af3185 100644 --- a/src/theory/quantifiers/single_inv_partition.h +++ b/src/theory/quantifiers/single_inv_partition.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H -#define __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H +#ifndef CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H +#define CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H #include <map> #include <vector> @@ -294,4 +294,4 @@ class SingleInvocationPartition } /* namespace CVC4::theory */ } /* namespace CVC4 */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */ diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp index 2f12c000c..1d2b869c4 100644 --- a/src/theory/quantifiers/skolemize.cpp +++ b/src/theory/quantifiers/skolemize.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h index 5605c8c5f..f07bbdfd3 100644 --- a/src/theory/quantifiers/skolemize.h +++ b/src/theory/quantifiers/skolemize.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H -#define __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H +#ifndef CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H +#define CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H #include <unordered_map> #include <unordered_set> @@ -143,4 +143,4 @@ class Skolemize } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SKOLEMIZE_H */ diff --git a/src/theory/quantifiers/solution_filter.cpp b/src/theory/quantifiers/solution_filter.cpp index 19d39e997..2c6186372 100644 --- a/src/theory/quantifiers/solution_filter.cpp +++ b/src/theory/quantifiers/solution_filter.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/solution_filter.h b/src/theory/quantifiers/solution_filter.h index d162f41f0..bd4c62a09 100644 --- a/src/theory/quantifiers/solution_filter.h +++ b/src/theory/quantifiers/solution_filter.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H -#define __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H +#ifndef CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H +#define CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H #include <map> #include <unordered_set> @@ -72,4 +72,4 @@ class SolutionFilterStrength : public ExprMiner } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SOLUTION_FILTER_H */ diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index aa20c1f76..00d040af5 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -2,9 +2,9 @@ /*! \file ce_guided_single_inv.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Andres Noetzli, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.h b/src/theory/quantifiers/sygus/ce_guided_single_inv.h index 0de7b4290..4b24cbb1c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H -#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H +#ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H +#define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_H #include "context/cdlist.h" #include "theory/quantifiers/sygus/ce_guided_single_inv_sol.h" diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp index 7f7c56f84..074971622 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.cpp @@ -2,9 +2,9 @@ /*! \file ce_guided_single_inv_sol.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds, Tim King, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h index fb0862413..40117af6c 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv_sol.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H -#define __CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H +#ifndef CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H +#define CVC4__THEORY__QUANTIFIERS__CE_GUIDED_SINGLE_INV_SOL_H #include "context/cdhashmap.h" #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 6aca71ca3..314b43711 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h index 849a39639..a295f6a40 100644 --- a/src/theory/quantifiers/sygus/cegis.h +++ b/src/theory/quantifiers/sygus/cegis.h @@ -2,9 +2,9 @@ /*! \file cegis.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli + ** Andrew Reynolds, Haniel Barbosa, FabianWolff ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__CEGIS_H -#define __CVC4__THEORY__QUANTIFIERS__CEGIS_H +#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_H +#define CVC4__THEORY__QUANTIFIERS__CEGIS_H #include <map> #include "theory/quantifiers/sygus/sygus_module.h" @@ -209,4 +209,4 @@ class Cegis : public SygusModule } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__CEGIS_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__CEGIS_H */ diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp index 18e313bf0..e34669425 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.cpp +++ b/src/theory/quantifiers/sygus/cegis_unif.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h index 972d07af7..a2e7be1c1 100644 --- a/src/theory/quantifiers/sygus/cegis_unif.h +++ b/src/theory/quantifiers/sygus/cegis_unif.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -13,8 +13,8 @@ **/ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS__CEGIS_UNIF_H #include <map> #include <vector> diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp index e8daa4256..b568b8f53 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.cpp +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/enum_stream_substitution.h b/src/theory/quantifiers/sygus/enum_stream_substitution.h index 476a364ea..687641e60 100644 --- a/src/theory/quantifiers/sygus/enum_stream_substitution.h +++ b/src/theory/quantifiers/sygus/enum_stream_substitution.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ **/ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS__ENUM_STREAM_SUBSTITUTION_H #include "expr/node.h" #include "theory/quantifiers/sygus/synth_conjecture.h" diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp index 9981b5141..bd85ea496 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp +++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -476,6 +476,13 @@ bool SygusEnumerator::TermEnumSlave::validateIndex() { Assert(d_index == tc.getNumTerms()); Trace("sygus-enum-debug2") << "slave(" << d_tn << ") : force master...\n"; + // if the size of the master is larger than the size limit, then + // there is no use continuing, since there are no more terms that this + // slave enumerator can return. + if (d_master->getCurrentSize() > d_sizeLim) + { + return false; + } // must push the master index if (!d_master->increment()) { @@ -655,9 +662,14 @@ bool SygusEnumerator::TermEnumMaster::increment() { return false; } + Trace("sygus-enum-summary") << "SygusEnumerator::TermEnumMaster: increment " + << d_tn << "..." << std::endl; d_isIncrementing = true; bool ret = incrementInternal(); d_isIncrementing = false; + Trace("sygus-enum-summary") + << "SygusEnumerator::TermEnumMaster: finished increment " << d_tn + << std::endl; return ret; } @@ -789,7 +801,15 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // restart with constructor class one (skip nullary constructors) d_consClassNum = 1; - return incrementInternal(); + + // We break for a round: return the null term when we cross a size + // boundary. This ensures that the necessary breaks are taken, e.g. + // in slave enumerators who may instead want to abandon this call to + // increment master when the size of the master makes their increment + // infeasible. + d_currTermSet = true; + d_currTerm = Node::null(); + return true; } bool incSuccess = false; @@ -819,6 +839,8 @@ bool SygusEnumerator::TermEnumMaster::incrementInternal() // the term was not unique based on rewriting Trace("sygus-enum-debug2") << "master(" << d_tn << "): failed addTerm\n"; + // we will return null (d_currTermSet is true at this point) + Assert(d_currTermSet); d_currTerm = Node::null(); } } diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.h b/src/theory/quantifiers/sygus/sygus_enumerator.h index 716a047d2..d4c466b03 100644 --- a/src/theory/quantifiers/sygus/sygus_enumerator.h +++ b/src/theory/quantifiers/sygus/sygus_enumerator.h @@ -1,10 +1,10 @@ -/******************** */ +/********************* */ /*! \file sygus_enumerator.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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H #include <map> #include <unordered_set> @@ -454,4 +454,4 @@ class SygusEnumerator : public EnumValGenerator } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_ENUMERATOR_H */ diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp index ac7467c00..e44b604d0 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h index 94f37c845..adc54c6a7 100644 --- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h +++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H #include <map> #include "expr/node.h" @@ -113,4 +113,4 @@ class SygusEvalUnfold } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EVAL_UNFOLD_H */ diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp index ddf52001e..f55ce2097 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.cpp +++ b/src/theory/quantifiers/sygus/sygus_explain.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_explain.h b/src/theory/quantifiers/sygus/sygus_explain.h index 3f18a65d6..ec29ab2a1 100644 --- a/src/theory/quantifiers/sygus/sygus_explain.h +++ b/src/theory/quantifiers/sygus/sygus_explain.h @@ -2,9 +2,9 @@ /*! \file sygus_explain.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, FabianWolff ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H #include <vector> @@ -241,4 +241,4 @@ class SygusExplain } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */ diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 67fa1398e..48da8e8e8 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h index bf377bd33..7dfa9b478 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h @@ -2,9 +2,9 @@ /*! \file sygus_grammar_cons.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_CONS_H #include "theory/quantifiers_engine.h" diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp index 8e41b6b07..fb6b23132 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h index 993d41668..ae701113c 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h @@ -2,9 +2,9 @@ /*! \file sygus_grammar_norm.h ** \verbatim ** Top contributors (to current version): - ** Haniel Barbosa, Tim King, Andrew Reynolds + ** Haniel Barbosa, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ **/ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H #include <map> #include <memory> diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp index 24aa74c9e..6ad590f28 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp @@ -2,9 +2,9 @@ /*! \file sygus_grammar_red.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.h b/src/theory/quantifiers/sygus/sygus_grammar_red.h index ce83402c9..8ed080a30 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_red.h +++ b/src/theory/quantifiers/sygus/sygus_grammar_red.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H #include <map> #include "theory/quantifiers_engine.h" @@ -116,4 +116,4 @@ class SygusRedundantCons } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_RED_H */ diff --git a/src/theory/quantifiers/sygus/sygus_invariance.cpp b/src/theory/quantifiers/sygus/sygus_invariance.cpp index 5ea01ef57..b494e085e 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.cpp +++ b/src/theory/quantifiers/sygus/sygus_invariance.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_invariance.h b/src/theory/quantifiers/sygus/sygus_invariance.h index 02c249411..feb2d3313 100644 --- a/src/theory/quantifiers/sygus/sygus_invariance.h +++ b/src/theory/quantifiers/sygus/sygus_invariance.h @@ -2,9 +2,9 @@ /*! \file sygus_invariance.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, Mathias Preiner, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H #include <unordered_map> #include <vector> @@ -300,4 +300,4 @@ class NegContainsSygusInvarianceTest : public SygusInvarianceTest } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_module.cpp b/src/theory/quantifiers/sygus/sygus_module.cpp index 3471472fa..42a125ae5 100644 --- a/src/theory/quantifiers/sygus/sygus_module.cpp +++ b/src/theory/quantifiers/sygus/sygus_module.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h index fef24e9bb..d5e1de3fc 100644 --- a/src/theory/quantifiers/sygus/sygus_module.h +++ b/src/theory/quantifiers/sygus/sygus_module.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H #include <map> #include "expr/node.h" @@ -148,4 +148,4 @@ class SygusModule } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_MODULE_H */ diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp index 7891814be..2ab51f1fb 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.cpp +++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp @@ -2,9 +2,9 @@ /*! \file sygus_pbe.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Aina Niemetz + ** Andrew Reynolds, Haniel Barbosa, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_pbe.h b/src/theory/quantifiers/sygus/sygus_pbe.h index dc7f1cc51..e82ce01da 100644 --- a/src/theory/quantifiers/sygus/sygus_pbe.h +++ b/src/theory/quantifiers/sygus/sygus_pbe.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_PBE_H #include "context/cdhashmap.h" #include "theory/quantifiers/sygus/sygus_module.h" diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.cpp b/src/theory/quantifiers/sygus/sygus_process_conj.cpp index a2454758a..2b9592d4d 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.cpp +++ b/src/theory/quantifiers/sygus/sygus_process_conj.cpp @@ -2,9 +2,9 @@ /*! \file sygus_process_conj.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_process_conj.h b/src/theory/quantifiers/sygus/sygus_process_conj.h index 199619699..e9ee340f4 100644 --- a/src/theory/quantifiers/sygus/sygus_process_conj.h +++ b/src/theory/quantifiers/sygus/sygus_process_conj.h @@ -2,9 +2,9 @@ /*! \file sygus_process_conj.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King + ** Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H #include <map> #include <unordered_map> diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp index 09525712f..85a0a4bf8 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp +++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp @@ -2,9 +2,9 @@ /*! \file sygus_repair_const.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -115,6 +115,7 @@ void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker, try { checker.reset(new SmtEngine(&em)); + checker->setIsInternalSubsolver(); checker->setTimeLimit(options::sygusRepairConstTimeout(), true); checker->setLogic(smt::currentSmtEngine()->getLogicInfo()); // renable options disabled by sygus diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h index c6bfd2806..bc3a58f9e 100644 --- a/src/theory/quantifiers/sygus/sygus_repair_const.h +++ b/src/theory/quantifiers/sygus/sygus_repair_const.h @@ -2,9 +2,9 @@ /*! \file sygus_repair_const.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H #include <unordered_set> #include "expr/node.h" @@ -215,4 +215,4 @@ class SygusRepairConst } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif.cpp b/src/theory/quantifiers/sygus/sygus_unif.cpp index 5d7017a1c..2eb508fde 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif.cpp @@ -2,9 +2,9 @@ /*! \file sygus_unif.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Andrew Reynolds, Aina Niemetz, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_unif.h b/src/theory/quantifiers/sygus/sygus_unif.h index 0784644f8..a5215628c 100644 --- a/src/theory/quantifiers/sygus/sygus_unif.h +++ b/src/theory/quantifiers/sygus/sygus_unif.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H #include <map> #include "expr/node.h" @@ -196,4 +196,4 @@ class SygusUnif } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.cpp b/src/theory/quantifiers/sygus/sygus_unif_io.cpp index c9db62735..207aa4c8e 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_io.cpp @@ -2,9 +2,9 @@ /*! \file sygus_unif_io.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Andrew Reynolds, Haniel Barbosa, Aina Niemetz ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -161,7 +161,12 @@ bool UnifContextIo::getStringIncrement(SygusUnifIo* sui, if (d_vals[j] == sui->d_true) { // example is active in this context - Assert(vals[j].isConst()); + if (!vals[j].isConst()) + { + // the value is unknown, thus we cannot use it to increment the strings + // position + return false; + } String mystr = vals[j].getConst<String>(); ival = mystr.size(); if (mystr.size() <= ex_vals[j].size()) @@ -199,7 +204,11 @@ bool UnifContextIo::isStringSolved(SygusUnifIo* sui, if (d_vals[j] == sui->d_true) { // example is active in this context - Assert(vals[j].isConst()); + if (!vals[j].isConst()) + { + // value is unknown, thus it does not solve + return false; + } String mystr = vals[j].getConst<String>(); if (ex_vals[j] != mystr) { @@ -448,12 +457,23 @@ void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals, ++it) { int new_status = status; - // if the current value is true + bool success = true; + // If the current value is true, then this is a relevant point. + // We must consider the value of this child. if (curr_val_true) { - if (status != 0) + if (it->first.isNull()) { - Assert(it->first.isConst() && it->first.getType().isBoolean()); + // The value of this child is unknown on this point, hence we + // do not recurse + success = false; + } + else if (status != 0) + { + // if the status is not zero (indicating that we have a mix of T/F), + // then we must compute the new status. + Assert(it->first.getType().isBoolean()); + Assert(it->first.isConst()); new_status = (it->first.getConst<bool>() ? 1 : -1); if (status != -2 && new_status != status) { @@ -461,7 +481,10 @@ void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals, } } } - it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + if (success) + { + it->second.getLeavesInternal(vals, pol, v, index + 1, new_status); + } } } } @@ -641,23 +664,41 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) for (unsigned j = 0, size = itsr->second.size(); j < size; j++) { Node res = itsr->second[j]; - Assert(res.isConst()); + // The value of this term for this example, or the truth value of + // the I/O pair if the role of this enumerator is enum_io. Node resb; if (eiv.getRole() == enum_io) { Node out = d_examples_out[j]; Assert(out.isConst()); - resb = res == out ? d_true : d_false; + // If the result is not constant, then we assume that it does + // not satisfy the example. This is a safe underapproximation + // of the good behavior of the current term, that is, we only + // produce solutions whose values are fully evaluatable on all input + // points. Notice that terms may be used as leaves of decision + // trees that are fully evaluatable on points in that branch, but + // are not evaluatable on others, e.g. (head x) in the solution: + // (ite ((_ is cons) x) (head x) 5) + resb = (res.isConst() && res == out) ? d_true : d_false; } else { - resb = res; + // We only set resb if it is constant, otherwise it remains null. + // This indicates its value cannot be determined. + if (res.isConst()) + { + resb = res; + } } cond_vals[resb] = true; results.push_back(resb); if (Trace.isOn("sygus-sui-enum")) { - if (resb.getType().isBoolean()) + if (resb.isNull()) + { + Trace("sygus-sui-enum") << "_"; + } + else if (resb.getType().isBoolean()) { Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0"); } @@ -677,6 +718,7 @@ void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) std::vector<Node> subsume; if (cond_vals.find(d_false) == cond_vals.end()) { + Assert(cond_vals.size() == 1); // it is the entire solution, we are done Trace("sygus-sui-enum") << " ...success, full solution added to PBE pool : " @@ -917,23 +959,27 @@ bool SygusUnifIo::getExplanationForEnumeratorExclude( std::vector<unsigned> cmp_indices; for (unsigned i = 0, size = results.size(); i < size; i++) { - Assert(results[i].isConst()); - Assert(d_examples_out[i].isConst()); - Trace("sygus-sui-cterm-debug") - << " " << results[i] << " <> " << d_examples_out[i]; - Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]); - Node contr = Rewriter::rewrite(cont); - if (contr == d_false) - { - cmp_indices.push_back(i); - Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl; - } - else + // If the result is not constant, then it is worthless. It does not + // impact whether the term is excluded. + if (results[i].isConst()) { - Trace("sygus-sui-cterm-debug") << "...contained." << std::endl; - if (isConditional) + Assert(d_examples_out[i].isConst()); + Trace("sygus-sui-cterm-debug") + << " " << results[i] << " <> " << d_examples_out[i]; + Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]); + Node contr = Rewriter::rewrite(cont); + if (contr == d_false) { - return false; + cmp_indices.push_back(i); + Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl; + } + else + { + Trace("sygus-sui-cterm-debug") << "...contained." << std::endl; + if (isConditional) + { + return false; + } } } } diff --git a/src/theory/quantifiers/sygus/sygus_unif_io.h b/src/theory/quantifiers/sygus/sygus_unif_io.h index 7f48645bf..7e9c5abd2 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_io.h +++ b/src/theory/quantifiers/sygus/sygus_unif_io.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H #include <map> #include "theory/quantifiers/sygus/sygus_unif.h" @@ -218,7 +218,24 @@ class SubsumeTrie int status, bool checkExistsOnly, bool checkSubsume); - /** helper function for above functions */ + /** helper function for above functions + * + * This adds to v[-1], v[0], v[1] the children of the trie that occur + * along paths that contain only false (v[-1]), a mix of true/false (v[0]), + * and only true (v[1]) values for respectively for relevant points. + * + * vals/pol is used to determine the relevant points, which impacts which + * paths of the trie to traverse on this call. + * In particular, all points such that (pol ? vals[index] : !vals[index]) + * are relevant. + * + * Paths that contain an unknown value for any relevant point are not + * traversed. In the larger picture, this ensures that terms are not used in a + * way such that their unknown value is relevant to the overall behavior of + * a synthesis solution. + * + * status holds the current value of v (0,1,-1) that we will be adding to. + */ void getLeavesInternal(const std::vector<Node>& vals, bool pol, std::map<int, std::vector<Node>>& v, @@ -472,4 +489,4 @@ class SygusUnifIo : public SygusUnif } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_IO_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp index ee07efdfe..3514ccbeb 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h index 179a5ac16..ada99dbaf 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_rl.h +++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Haniel Barbosa, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H #include <map> #include "options/main_options.h" @@ -434,4 +434,4 @@ class SygusUnifRl : public SygusUnif } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */ diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp index 3cbac1eaa..acf5a2d7f 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.h b/src/theory/quantifiers/sygus/sygus_unif_strat.h index 41923f7a1..1c691bd84 100644 --- a/src/theory/quantifiers/sygus/sygus_unif_strat.h +++ b/src/theory/quantifiers/sygus/sygus_unif_strat.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Haniel Barbosa, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_STRAT_H #include <map> #include "expr/node.h" @@ -429,4 +429,4 @@ class SygusUnifStrategy } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_H */ diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp index e25e8a225..756e1f791 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.cpp +++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp @@ -2,9 +2,9 @@ /*! \file synth_conjecture.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Haniel Barbosa + ** Andrew Reynolds, Haniel Barbosa, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -540,6 +540,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) Trace("cegqi-engine") << "Check side condition..." << std::endl; Trace("cegqi-debug") << "Check side condition : " << sc << std::endl; SmtEngine scSmt(nm->toExprManager()); + scSmt.setIsInternalSubsolver(); scSmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); scSmt.assertFormula(sc.toExpr()); Result r = scSmt.checkSat(); @@ -572,6 +573,7 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems) { Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl; SmtEngine verifySmt(nm->toExprManager()); + verifySmt.setIsInternalSubsolver(); verifySmt.setLogic(smt::currentSmtEngine()->getLogicInfo()); verifySmt.assertFormula(query.toExpr()); Result r = verifySmt.checkSat(); diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h index cf6178fdb..83a7eaa45 100644 --- a/src/theory/quantifiers/sygus/synth_conjecture.h +++ b/src/theory/quantifiers/sygus/synth_conjecture.h @@ -2,9 +2,9 @@ /*! \file synth_conjecture.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Haniel Barbosa + ** Andrew Reynolds, Haniel Barbosa, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H -#define __CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H +#define CVC4__THEORY__QUANTIFIERS__SYNTH_CONJECTURE_H #include <memory> diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp index d3eff1750..fc1ed938d 100644 --- a/src/theory/quantifiers/sygus/synth_engine.cpp +++ b/src/theory/quantifiers/sygus/synth_engine.cpp @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -159,6 +159,7 @@ void SynthEngine::assignConjecture(Node q) { // create new smt engine to do quantifier elimination SmtEngine smt_qe(nm->toExprManager()); + smt_qe.setIsInternalSubsolver(); smt_qe.setLogic(smt::currentSmtEngine()->getLogicInfo()); Trace("cegqi-qep") << "Property is non-ground single invocation, run " "QE to obtain single invocation." diff --git a/src/theory/quantifiers/sygus/synth_engine.h b/src/theory/quantifiers/sygus/synth_engine.h index a7346b888..d5337e5d1 100644 --- a/src/theory/quantifiers/sygus/synth_engine.h +++ b/src/theory/quantifiers/sygus/synth_engine.h @@ -2,9 +2,9 @@ /*! \file synth_engine.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner, Tim King + ** Andrew Reynolds, Mathias Preiner, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -15,8 +15,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H -#define __CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H +#define CVC4__THEORY__QUANTIFIERS__SYNTH_ENGINE_H #include "context/cdhashmap.h" #include "theory/quantifiers/sygus/synth_conjecture.h" diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp index 9198f7e56..af820b0fc 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.cpp +++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp @@ -2,9 +2,9 @@ /*! \file term_database_sygus.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa, Aina Niemetz + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -1633,6 +1633,33 @@ Node TermDbSygus::evaluateWithUnfolding( while (ret.getKind() == DT_SYGUS_EVAL && ret[0].getKind() == APPLY_CONSTRUCTOR) { + if (ret == n && ret[0].isConst()) + { + Trace("dt-eval-unfold-debug") + << "Optimize: evaluate constant head " << ret << std::endl; + // can just do direct evaluation here + std::vector<Node> args; + bool success = true; + for (unsigned i = 1, nchild = ret.getNumChildren(); i < nchild; i++) + { + if (!ret[i].isConst()) + { + success = false; + break; + } + args.push_back(ret[i]); + } + if (success) + { + TypeNode rt = ret[0].getType(); + Node bret = sygusToBuiltin(ret[0], rt); + Node rete = evaluateBuiltin(rt, bret, args); + visited[n] = rete; + Trace("dt-eval-unfold-debug") + << "Return " << rete << " for " << n << std::endl; + return rete; + } + } ret = unfold( ret ); } if( ret.getNumChildren()>0 ){ diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h index 7a522ded6..0f3d650d3 100644 --- a/src/theory/quantifiers/sygus/term_database_sygus.h +++ b/src/theory/quantifiers/sygus/term_database_sygus.h @@ -2,9 +2,9 @@ /*! \file term_database_sygus.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds + ** Andrew Reynolds, Andres Noetzli, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H -#define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H +#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H +#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_SYGUS_H #include <unordered_set> @@ -599,4 +599,4 @@ class TermDbSygus { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp index f1908fc19..10d7ef6ab 100644 --- a/src/theory/quantifiers/sygus_sampler.cpp +++ b/src/theory/quantifiers/sygus_sampler.cpp @@ -2,9 +2,9 @@ /*! \file sygus_sampler.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Haniel Barbosa + ** Andrew Reynolds, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -40,7 +40,6 @@ void SygusSampler::initialize(TypeNode tn, d_tds = nullptr; d_use_sygus_type = false; d_is_valid = true; - d_tn = tn; d_ftn = TypeNode::null(); d_type_vars.clear(); d_vars.clear(); @@ -95,7 +94,6 @@ void SygusSampler::initializeSygus(TermDbSygus* tds, Assert(d_ftn.isDatatype()); const Datatype& dt = static_cast<DatatypeType>(d_ftn.toType()).getDatatype(); Assert(dt.isSygus()); - d_tn = TypeNode::fromType(dt.getSygusType()); Trace("sygus-sample") << "Register sampler for " << f << std::endl; @@ -264,28 +262,30 @@ bool SygusSampler::PtTrie::add(std::vector<Node>& pt) Node SygusSampler::registerTerm(Node n, bool forceKeep) { - if (d_is_valid) + if (!d_is_valid) { - Node bn = n; - // if this is a sygus type, get its builtin analog - if (d_use_sygus_type) - { - Assert(!d_ftn.isNull()); - bn = d_tds->sygusToBuiltin(n); - Assert(d_builtin_to_sygus.find(bn) == d_builtin_to_sygus.end() - || d_builtin_to_sygus[bn] == n); - d_builtin_to_sygus[bn] = n; - } - Assert(bn.getType() == d_tn); - Node res = d_trie.add(bn, this, 0, d_samples.size(), forceKeep); - if (d_use_sygus_type) - { - Assert(d_builtin_to_sygus.find(res) != d_builtin_to_sygus.end()); - res = res != bn ? d_builtin_to_sygus[res] : n; - } - return res; + // do nothing + return n; + } + Node bn = n; + TypeNode tn = n.getType(); + // If we are using sygus types, get the builtin analog of n. + if (d_use_sygus_type) + { + bn = d_tds->sygusToBuiltin(n); + d_builtin_to_sygus[tn][bn] = n; + } + // cache based on the (original) type of n + Node res = d_trie[tn].add(bn, this, 0, d_samples.size(), forceKeep); + // If we are using sygus types, map back to an original. + // Notice that d_builtin_to_sygus is not necessarily bijective. + if (d_use_sygus_type) + { + std::map<Node, Node>& bts = d_builtin_to_sygus[tn]; + Assert(bts.find(res) != bts.end()); + res = res != bn ? bts[res] : n; } - return n; + return res; } bool SygusSampler::isContiguous(Node n) diff --git a/src/theory/quantifiers/sygus_sampler.h b/src/theory/quantifiers/sygus_sampler.h index 28f715b34..429b6f511 100644 --- a/src/theory/quantifiers/sygus_sampler.h +++ b/src/theory/quantifiers/sygus_sampler.h @@ -2,9 +2,9 @@ /*! \file sygus_sampler.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Mathias Preiner + ** Andrew Reynolds, FabianWolff, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H -#define __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H +#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H +#define CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H #include <map> #include "theory/evaluator.h" @@ -194,14 +194,15 @@ class SygusSampler : public LazyTrieEvaluator }; /** a trie for samples */ PtTrie d_samples_trie; - /** type of nodes we will be registering with this class */ - TypeNode d_tn; /** the sygus type for this sampler (if applicable). */ TypeNode d_ftn; - /** whether we are registering terms of type d_ftn */ + /** whether we are registering terms of sygus types with this sampler */ bool d_use_sygus_type; - /** map from builtin terms to the sygus term they correspond to */ - std::map<Node, Node> d_builtin_to_sygus; + /** + * For each (sygus) type, a map from builtin terms to the sygus term they + * correspond to. + */ + std::map<TypeNode, std::map<Node, Node> > d_builtin_to_sygus; /** all variables we are sampling values for */ std::vector<Node> d_vars; /** type variables @@ -235,8 +236,22 @@ class SygusSampler : public LazyTrieEvaluator * that type. */ std::map<TypeNode, std::vector<Node> > d_type_consts; - /** the lazy trie */ - LazyTrie d_trie; + /** a lazy trie for each type + * + * This stores the evaluation of all terms registered to this class. + * + * Notice if we are registering sygus terms with this class, then terms + * are grouped into this trie according to their sygus type, and not their + * builtin type. For example, for grammar: + * A -> x | B+1 + * B -> x | 0 | 1 | B+B + * If we register C^B_+( C^B_x(), C^B_0() ) and C^A_x() with this class, + * then x+0 is registered to d_trie[B] and x is registered to d_trie[A], + * and no rewrite rule is reported. The reason for this is that otherwise + * we would end up reporting many useless rewrites since the same builtin + * term can be generated by multiple sygus types (e.g. C^B_x() and C^A_x()). + */ + std::map<TypeNode, LazyTrie> d_trie; /** is this sampler valid? * * A sampler can be invalid if sample points cannot be generated for a type @@ -307,4 +322,4 @@ class SygusSampler : public LazyTrieEvaluator } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_SAMPLER_H */ diff --git a/src/theory/quantifiers/term_canonize.cpp b/src/theory/quantifiers/term_canonize.cpp index d257198d9..9817da5a1 100644 --- a/src/theory/quantifiers/term_canonize.cpp +++ b/src/theory/quantifiers/term_canonize.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/term_canonize.h b/src/theory/quantifiers/term_canonize.h index e23627271..8f7b8722e 100644 --- a/src/theory/quantifiers/term_canonize.h +++ b/src/theory/quantifiers/term_canonize.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H -#define __CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H +#ifndef CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H +#define CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H #include <map> #include "expr/node.h" @@ -89,4 +89,4 @@ class TermCanonize } // namespace theory } // namespace CVC4 -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_CANONIZE_H */ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 44c5586c3..abb84ccd7 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -2,9 +2,9 @@ /*! \file term_database.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Tim King, Francois Bobot + ** Andrew Reynolds, Tim King, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -228,7 +228,7 @@ void TermDb::addTerm(Node n, d_iclosure_processed.insert(n); rec = true; } - if (rec && n.getKind() != FORALL) + if (rec && !n.isClosure()) { for (const Node& nc : n) { @@ -509,88 +509,196 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) { } } -//return a term n' equivalent to n -// maximal subterms of n' are representatives in the equality engine qy -Node TermDb::evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ) { +Node TermDb::evaluateTerm2(TNode n, + std::map<TNode, Node>& visited, + std::vector<Node>& exp, + EqualityQuery* qy, + bool useEntailmentTests, + bool computeExp, + bool reqHasTerm) +{ std::map< TNode, Node >::iterator itv = visited.find( n ); if( itv != visited.end() ){ return itv->second; } + size_t prevSize = exp.size(); Trace("term-db-eval") << "evaluate term : " << n << std::endl; Node ret = n; if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){ //do nothing - }else if( !qy->hasTerm( n ) ){ - //term is not known to be equal to a representative in equality engine, evaluate it - if( n.hasOperator() ){ - TNode f = getMatchOperator( n ); - std::vector< TNode > args; - bool ret_set = false; - for( unsigned i=0; i<n.getNumChildren(); i++ ){ - TNode c = evaluateTerm2( n[i], visited, qy, useEntailmentTests ); - if( c.isNull() ){ - ret = Node::null(); + } + else if (qy->hasTerm(n)) + { + Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; + ret = qy->getRepresentative(n); + if (computeExp) + { + if (n != ret) + { + exp.push_back(n.eqNode(ret)); + } + } + reqHasTerm = false; + } + else if (n.hasOperator()) + { + std::vector<TNode> args; + bool ret_set = false; + Kind k = n.getKind(); + std::vector<Node> tempExp; + for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++) + { + TNode c = evaluateTerm2(n[i], + visited, + tempExp, + qy, + useEntailmentTests, + computeExp, + reqHasTerm); + if (c.isNull()) + { + ret = Node::null(); + ret_set = true; + break; + } + else if (c == d_true || c == d_false) + { + // short-circuiting + if ((k == AND && c == d_false) || (k == OR && c == d_true)) + { + ret = c; + ret_set = true; + reqHasTerm = false; + break; + } + else if (k == ITE && i == 0) + { + ret = evaluateTerm2(n[c == d_true ? 1 : 2], + visited, + tempExp, + qy, + useEntailmentTests, + computeExp, + reqHasTerm); ret_set = true; + reqHasTerm = false; break; - }else if( c==d_true || c==d_false ){ - //short-circuiting - if( ( n.getKind()==kind::AND && c==d_false ) || ( n.getKind()==kind::OR && c==d_true ) ){ - ret = c; - ret_set = true; - break; - }else if( n.getKind()==kind::ITE && i==0 ){ - ret = evaluateTerm2( n[ c==d_true ? 1 : 2], visited, qy, useEntailmentTests ); - ret_set = true; - break; + } + } + if (computeExp) + { + exp.insert(exp.end(), tempExp.begin(), tempExp.end()); + } + Trace("term-db-eval") << " child " << i << " : " << c << std::endl; + args.push_back(c); + } + if (ret_set) + { + // if we short circuited + if (computeExp) + { + exp.clear(); + exp.insert(exp.end(), tempExp.begin(), tempExp.end()); + } + } + else + { + // get the (indexed) operator of n, if it exists + TNode f = getMatchOperator(n); + // if it is an indexed term, return the congruent term + if (!f.isNull()) + { + // if f is congruent to a term indexed by this class + TNode nn = qy->getCongruentTerm(f, args); + Trace("term-db-eval") << " got congruent term " << nn + << " from DB for " << n << std::endl; + if (!nn.isNull()) + { + if (computeExp) + { + Assert(nn.getNumChildren() == n.getNumChildren()); + for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++) + { + if (nn[i] != n[i]) + { + exp.push_back(nn[i].eqNode(n[i])); + } + } + } + ret = qy->getRepresentative(nn); + Trace("term-db-eval") << "return rep" << std::endl; + ret_set = true; + reqHasTerm = false; + Assert(!ret.isNull()); + if (computeExp) + { + if (n != ret) + { + exp.push_back(nn.eqNode(ret)); + } } } - Trace("term-db-eval") << " child " << i << " : " << c << std::endl; - args.push_back( c ); } if( !ret_set ){ - //if it is an indexed term, return the congruent term - if( !f.isNull() ){ - TNode nn = qy->getCongruentTerm( f, args ); - Trace("term-db-eval") << " got congruent term " << nn << " from DB for " << n << std::endl; - if( !nn.isNull() ){ - ret = qy->getRepresentative( nn ); - Trace("term-db-eval") << "return rep" << std::endl; - ret_set = true; - Assert( !ret.isNull() ); - } + Trace("term-db-eval") << "return rewrite" << std::endl; + // a theory symbol or a new UF term + if (n.getMetaKind() == metakind::PARAMETERIZED) + { + args.insert(args.begin(), n.getOperator()); } - if( !ret_set ){ - Trace("term-db-eval") << "return rewrite" << std::endl; - //a theory symbol or a new UF term - if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){ - args.insert( args.begin(), n.getOperator() ); - } - ret = NodeManager::currentNM()->mkNode( n.getKind(), args ); - ret = Rewriter::rewrite( ret ); - if( ret.getKind()==kind::EQUAL ){ - if( qy->areDisequal( ret[0], ret[1] ) ){ - ret = d_false; - } + ret = NodeManager::currentNM()->mkNode(n.getKind(), args); + ret = Rewriter::rewrite(ret); + if (ret.getKind() == EQUAL) + { + if (qy->areDisequal(ret[0], ret[1])) + { + ret = d_false; } - if( useEntailmentTests ){ - if( ret.getKind()==kind::EQUAL || ret.getKind()==kind::GEQ ){ - for( unsigned j=0; j<2; j++ ){ - std::pair<bool, Node> et = d_quantEngine->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, j==0 ? ret : ret.negate() ); - if( et.first ){ - ret = j==0 ? d_true : d_false; - break; + } + if (useEntailmentTests) + { + if (ret.getKind() == EQUAL || ret.getKind() == GEQ) + { + TheoryEngine* te = d_quantEngine->getTheoryEngine(); + for (unsigned j = 0; j < 2; j++) + { + std::pair<bool, Node> et = te->entailmentCheck( + THEORY_OF_TYPE_BASED, j == 0 ? ret : ret.negate()); + if (et.first) + { + ret = j == 0 ? d_true : d_false; + if (computeExp) + { + exp.push_back(et.second); } + break; } } } } } } - }else{ - Trace("term-db-eval") << "...exists in ee, return rep" << std::endl; - ret = qy->getRepresentative( n ); } - Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret << std::endl; + // must have the term + if (reqHasTerm && !ret.isNull()) + { + Kind k = ret.getKind(); + if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT + && k != FORALL) + { + if (!qy->hasTerm(ret)) + { + ret = Node::null(); + } + } + } + Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret + << ", reqHasTerm = " << reqHasTerm << std::endl; + // clear the explanation if failed + if (computeExp && ret.isNull()) + { + exp.resize(prevSize); + } visited[n] = ret; return ret; } @@ -645,12 +753,33 @@ TNode TermDb::getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool su return TNode::null(); } -Node TermDb::evaluateTerm( TNode n, EqualityQuery * qy, bool useEntailmentTests ) { +Node TermDb::evaluateTerm(TNode n, + EqualityQuery* qy, + bool useEntailmentTests, + bool reqHasTerm) +{ if( qy==NULL ){ qy = d_quantEngine->getEqualityQuery(); } std::map< TNode, Node > visited; - return evaluateTerm2( n, visited, qy, useEntailmentTests ); + std::vector<Node> exp; + return evaluateTerm2( + n, visited, exp, qy, useEntailmentTests, false, reqHasTerm); +} + +Node TermDb::evaluateTerm(TNode n, + std::vector<Node>& exp, + EqualityQuery* qy, + bool useEntailmentTests, + bool reqHasTerm) +{ + if (qy == NULL) + { + qy = d_quantEngine->getEqualityQuery(); + } + std::map<TNode, Node> visited; + return evaluateTerm2( + n, visited, exp, qy, useEntailmentTests, true, reqHasTerm); } TNode TermDb::getEntailedTerm( TNode n, std::map< TNode, TNode >& subs, bool subsRep, EqualityQuery * qy ) { diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index cc9a24d08..148a18958 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H -#define __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H +#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H +#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H #include <map> #include <unordered_set> @@ -178,17 +178,37 @@ class TermDb : public QuantifiersUtil { bool inRelevantDomain(TNode f, unsigned i, TNode r); /** evaluate term * - * Returns a term n' such that n = n' is entailed based on the equality - * information qy. This function may generate new terms. In particular, - * we typically rewrite maximal - * subterms of n to terms that exist in the equality engine specified by qy. - * - * useEntailmentTests is whether to use the theory engine's entailmentCheck - * call, for increased precision. This is not frequently used. - */ + * Returns a term n' such that n = n' is entailed based on the equality + * information qy. This function may generate new terms. In particular, + * we typically rewrite subterms of n of maximal size to terms that exist in + * the equality engine specified by qy. + * + * useEntailmentTests is whether to call the theory engine's entailmentTest + * on literals n for which this call fails to find a term n' that is + * equivalent to n, for increased precision. This is not frequently used. + * + * The vector exp stores the explanation for why n evaluates to that term, + * that is, if this call returns a non-null node n', then: + * exp => n = n' + * + * If reqHasTerm, then we require that the returned term is a Boolean + * combination of terms that exist in the equality engine used by this call. + * If no such term is constructable, this call returns null. The motivation + * for setting this to true is to "fail fast" if we require the return value + * of this function to only involve existing terms. This is used e.g. in + * the "propagating instances" portion of conflict-based instantiation + * (quant_conflict_find.h). + */ + Node evaluateTerm(TNode n, + std::vector<Node>& exp, + EqualityQuery* qy = NULL, + bool useEntailmentTests = false, + bool reqHasTerm = false); + /** same as above, without exp */ Node evaluateTerm(TNode n, EqualityQuery* qy = NULL, - bool useEntailmentTests = false); + bool useEntailmentTests = false, + bool reqHasTerm = false); /** get entailed term * * If possible, returns a term n' such that: @@ -307,7 +327,13 @@ class TermDb : public QuantifiersUtil { /** set has term */ void setHasTerm( Node n ); /** helper for evaluate term */ - Node evaluateTerm2( TNode n, std::map< TNode, Node >& visited, EqualityQuery * qy, bool useEntailmentTests ); + Node evaluateTerm2(TNode n, + std::map<TNode, Node>& visited, + std::vector<Node>& exp, + EqualityQuery* qy, + bool useEntailmentTests, + bool computeExp, + bool reqHasTerm); /** helper for get entailed term */ TNode getEntailedTerm2( TNode n, std::map< TNode, TNode >& subs, bool subsRep, bool hasSubs, EqualityQuery * qy ); /** helper for is entailed */ @@ -383,4 +409,4 @@ class TermDb : public QuantifiersUtil { }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp index 8e3219768..0336700ad 100644 --- a/src/theory/quantifiers/term_enumeration.cpp +++ b/src/theory/quantifiers/term_enumeration.cpp @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -87,6 +87,26 @@ bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard) return mc; } +bool TermEnumeration::getDomain(TypeNode tn, std::vector<Node>& dom) +{ + if (!mayComplete(tn)) + { + return false; + } + Node curre; + unsigned counter = 0; + do + { + curre = getEnumerateTerm(tn, counter); + counter++; + if (!curre.isNull()) + { + dom.push_back(curre); + } + } while (!curre.isNull()); + return true; +} + } /* CVC4::theory::quantifiers namespace */ } /* CVC4::theory namespace */ } /* CVC4 namespace */ diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h index cf25335f4..279680b1f 100644 --- a/src/theory/quantifiers/term_enumeration.h +++ b/src/theory/quantifiers/term_enumeration.h @@ -4,7 +4,7 @@ ** 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 + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H -#define __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H +#ifndef CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H +#define CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H #include <unordered_map> #include <vector> @@ -56,6 +56,14 @@ class TermEnumeration */ static bool mayComplete(TypeNode tn, unsigned cardMax); + /** get domain + * + * If tn is a type such that mayComplete(tn) returns true, this method + * adds all domain elements of tn to dom and returns true. Otherwise, this + * method returns false. + */ + bool getDomain(TypeNode tn, std::vector<Node>& dom); + private: /** ground terms enumerated for types */ std::unordered_map<TypeNode, std::vector<Node>, TypeNodeHashFunction> @@ -74,4 +82,4 @@ class TermEnumeration } /* CVC4::theory namespace */ } /* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_ENUMERATION_H */ diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 4c9cf2c8d..065096607 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -2,9 +2,9 @@ /*! \file term_util.cpp ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Paul Meng, Yoni Zohar + ** Andrew Reynolds, Morgan Deters, Andres Noetzli ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 820821991..1f2eea1c5 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -2,9 +2,9 @@ /*! \file term_util.h ** \verbatim ** Top contributors (to current version): - ** Andrew Reynolds, Mathias Preiner + ** Andrew Reynolds, Morgan Deters, Mathias Preiner ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -14,8 +14,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H -#define __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H +#ifndef CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H +#define CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H #include <map> #include <unordered_set> @@ -379,4 +379,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__TERM_UTIL_H */ diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index 6f647aeb1..f24a4bb2b 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -2,9 +2,9 @@ /*! \file theory_quantifiers.cpp ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Andrew Reynolds, Tim King + ** Andrew Reynolds, Morgan Deters, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -38,8 +38,6 @@ using namespace CVC4::theory::quantifiers; TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) : Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo) { - d_numInstantiations = 0; - d_baseDecLevel = -1; out.handleUserAttribute( "axiom", this ); out.handleUserAttribute( "conjecture", this ); out.handleUserAttribute( "fun-def", this ); @@ -71,13 +69,6 @@ void TheoryQuantifiers::preRegisterTerm(TNode n) { return; } Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl; - if (options::cbqi() && !options::recurseCbqi() - && TermUtil::hasInstConstAttr(n)) - { - Debug("quantifiers-prereg") - << "TheoryQuantifiers::preRegisterTerm() done, unused " << n << endl; - return; - } // Preregister the quantified formula. // This initializes the modules used for handling n in this user context. getQuantifiersEngine()->preRegisterQuantifier(n); @@ -135,7 +126,7 @@ void TheoryQuantifiers::check(Effort e) { Trace("quantifiers-assert") << "quantifiers::assert(): " << assertion << std::endl; switch(assertion.getKind()) { case kind::FORALL: - assertUniversal( assertion ); + getQuantifiersEngine()->assertQuantifier(assertion, true); break; case kind::INST_CLOSURE: getQuantifiersEngine()->addTermToDatabase( assertion[0], false, true ); @@ -150,7 +141,7 @@ void TheoryQuantifiers::check(Effort e) { { switch( assertion[0].getKind()) { case kind::FORALL: - assertExistential( assertion ); + getQuantifiersEngine()->assertQuantifier(assertion[0], false); break; case kind::EQUAL: //do nothing @@ -171,20 +162,6 @@ void TheoryQuantifiers::check(Effort e) { getQuantifiersEngine()->check( e ); } -void TheoryQuantifiers::assertUniversal( Node n ){ - Assert( n.getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n) ){ - getQuantifiersEngine()->assertQuantifier( n, true ); - } -} - -void TheoryQuantifiers::assertExistential( Node n ){ - Assert( n.getKind()== NOT && n[0].getKind()==FORALL ); - if( !options::cbqi() || options::recurseCbqi() || !TermUtil::hasInstConstAttr(n[0]) ){ - getQuantifiersEngine()->assertQuantifier( n[0], false ); - } -} - void TheoryQuantifiers::setUserAttribute(const std::string& attr, Node n, std::vector<Node> node_values, std::string str_value){ QuantAttributes::setUserAttribute( attr, n, node_values, str_value ); } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index 55047fe2b..b5b07f2e6 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -2,9 +2,9 @@ /*! \file theory_quantifiers.h ** \verbatim ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds + ** Tim King, Morgan Deters, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H -#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H +#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H +#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H #include "context/cdhashmap.h" #include "context/context.h" @@ -56,17 +56,10 @@ class TheoryQuantifiers : public Theory { std::vector<Node> node_values, std::string str_value) override; - private: - void assertUniversal( Node n ); - void assertExistential( Node n ); - /** number of instantiations */ - int d_numInstantiations; - int d_baseDecLevel; - };/* class TheoryQuantifiers */ }/* CVC4::theory::quantifiers namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_H */ diff --git a/src/theory/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h index bac3ca58f..ad1c4c69b 100644 --- a/src/theory/quantifiers/theory_quantifiers_type_rules.h +++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h @@ -4,7 +4,7 @@ ** Top contributors (to current version): ** Morgan Deters, Andrew Reynolds, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** Copyright (c) 2009-2019 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 @@ -16,8 +16,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H -#define __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H +#ifndef CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H +#define CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H #include "expr/matcher.h" @@ -229,4 +229,4 @@ public: }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */ +#endif /* CVC4__THEORY__QUANTIFIERS__THEORY_QUANTIFIERS_TYPE_RULES_H */ |