diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-09-02 20:41:08 +0000 |
| commit | 1d18e5ebed9a5b20ed6a8fe21d11842acf6fa7ea (patch) | |
| tree | 7074f04453914bc377ff6aeb307dd17b82b76ff3 /src/theory | |
| parent | 74770f1071e6102795393cf65dd0c651038db6b4 (diff) | |
Merge from my post-smtcomp branch. Includes:
Dumping infrastructure. Can dump preprocessed queries and clauses. Can
also dump queries (for testing with another solver) to see if any conflicts
are missed, T-propagations are missed, all lemmas are T-valid, etc. For a
full list of options see --dump=help.
CUDD building much cleaner.
Documentation and assertion fixes.
Printer improvements, printing of commands in language-defined way, etc.
Typechecker stuff in expr package now autogenerated, no need to manually
edit the expr package when adding a new theory.
CVC3 compatibility layer (builds as libcompat).
SWIG detection and language binding support (infrastructure).
Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode
(when not in compliance mode).
Copyright and file headers regenerated.
Diffstat (limited to 'src/theory')
112 files changed, 654 insertions, 2573 deletions
diff --git a/src/theory/arith/arith_priority_queue.cpp b/src/theory/arith/arith_priority_queue.cpp index 872c25e3b..3b1f5f395 100644 --- a/src/theory/arith/arith_priority_queue.cpp +++ b/src/theory/arith/arith_priority_queue.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_priority_queue.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/arith_priority_queue.h" diff --git a/src/theory/arith/arith_priority_queue.h b/src/theory/arith/arith_priority_queue.h index f912d7753..1e7e3460b 100644 --- a/src/theory/arith/arith_priority_queue.h +++ b/src/theory/arith/arith_priority_queue.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_priority_queue.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" diff --git a/src/theory/arith/arith_prop_manager.cpp b/src/theory/arith/arith_prop_manager.cpp index 7f38c74a7..d1fce5b90 100644 --- a/src/theory/arith/arith_prop_manager.cpp +++ b/src/theory/arith/arith_prop_manager.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_prop_manager.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/arith_prop_manager.h" diff --git a/src/theory/arith/arith_prop_manager.h b/src/theory/arith/arith_prop_manager.h index 39bcb7477..82f58c7a0 100644 --- a/src/theory/arith/arith_prop_manager.h +++ b/src/theory/arith/arith_prop_manager.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file arith_prop_manager.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" #ifndef __CVC4__THEORY__ARITH__ARITH_PROP_MANAGER_H diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 8d12e78fe..66223b479 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -2,8 +2,8 @@ /*! \file arith_rewriter.cpp ** \verbatim ** Original author: taking - ** Major contributors: dejan - ** Minor contributors (to current version): mdeters + ** Major contributors: none + ** Minor contributors (to current version): mdeters, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h index c58778215..03402a6f1 100644 --- a/src/theory/arith/arith_static_learner.h +++ b/src/theory/arith/arith_static_learner.h @@ -2,8 +2,8 @@ /*! \file arith_static_learner.h ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: mdeters + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 2dee26be4..3a1135f74 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/atom_database.cpp b/src/theory/arith/atom_database.cpp index 5c3519435..774d0eb22 100644 --- a/src/theory/arith/atom_database.cpp +++ b/src/theory/arith/atom_database.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/atom_database.h b/src/theory/arith/atom_database.h index 25020977a..af7068ada 100644 --- a/src/theory/arith/atom_database.h +++ b/src/theory/arith/atom_database.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp index d0e4ed1f4..c5c5c629b 100644 --- a/src/theory/arith/delta_rational.cpp +++ b/src/theory/arith/delta_rational.cpp @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index c70d26db5..c8a5e39a7 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds index db47062bb..bf5ea24c1 100644 --- a/src/theory/arith/kinds +++ b/src/theory/arith/kinds @@ -5,6 +5,7 @@ # theory THEORY_ARITH ::CVC4::theory::arith::TheoryArith "theory/arith/theory_arith.h" +typechecker "theory/arith/theory_arith_type_rules.h" properties stable-infinite properties check propagate staticLearning presolve notifyRestart @@ -17,6 +18,7 @@ operator MULT 2: "arithmetic multiplication" operator MINUS 2 "arithmetic binary subtraction operator" operator UMINUS 1 "arithmetic unary negation" operator DIVISION 2 "arithmetic division" +operator POW 2 "arithmetic power" sort REAL_TYPE \ Cardinality::REALS \ @@ -58,4 +60,19 @@ operator LEQ 2 "less than or equal, x <= y" operator GT 2 "greater than, x > y" operator GEQ 2 "greater than or equal, x >= y" +typerule PLUS ::CVC4::theory::arith::ArithOperatorTypeRule +typerule MULT ::CVC4::theory::arith::ArithOperatorTypeRule +typerule MINUS ::CVC4::theory::arith::ArithOperatorTypeRule +typerule UMINUS ::CVC4::theory::arith::ArithOperatorTypeRule +typerule DIVISION ::CVC4::theory::arith::ArithOperatorTypeRule +typerule POW ::CVC4::theory::arith::ArithOperatorTypeRule + +typerule CONST_RATIONAL ::CVC4::theory::arith::ArithConstantTypeRule +typerule CONST_INTEGER ::CVC4::theory::arith::ArithConstantTypeRule + +typerule LT ::CVC4::theory::arith::ArithPredicateTypeRule +typerule LEQ ::CVC4::theory::arith::ArithPredicateTypeRule +typerule GT ::CVC4::theory::arith::ArithPredicateTypeRule +typerule GEQ ::CVC4::theory::arith::ArithPredicateTypeRule + endtheory diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index b529a8077..e7df14df7 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index d6e79318d..6e2d706cc 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/ordered_set.h b/src/theory/arith/ordered_set.h index e44ba8687..c126ab568 100644 --- a/src/theory/arith/ordered_set.h +++ b/src/theory/arith/ordered_set.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file ordered_set.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include <map> #include <set> #include "expr/kind.h" diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp index 3cd8ed926..ed8f837d1 100644 --- a/src/theory/arith/partial_model.cpp +++ b/src/theory/arith/partial_model.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h index f07e524aa..aa333046b 100644 --- a/src/theory/arith/partial_model.h +++ b/src/theory/arith/partial_model.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 3e2d90674..77e7e1060 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file simplex.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/arith/simplex.h" diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h index b3f43baf1..04b4ca784 100644 --- a/src/theory/arith/simplex.h +++ b/src/theory/arith/simplex.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file simplex.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4_private.h" diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index b432416bd..ef3206650 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index e14436f8c..3da3d68a5 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -2,10 +2,10 @@ /*! \file tableau.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan + ** Major contributors: none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 2664aaac3..4369c6de0 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -2,10 +2,10 @@ /*! \file theory_arith.cpp ** \verbatim ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): barrett, dejan, mdeters + ** Major contributors: mdeters, dejan + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 7e14f6b06..2e85659e4 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: taking - ** Minor contributors (to current version): barrett + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index 8bfd2aef6..9c69ec684 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp index 5a836fdc2..1e06621b4 100644 --- a/src/theory/arrays/array_info.cpp +++ b/src/theory/arrays/array_info.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: lianah ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index ce3f015b5..fcc45bbd5 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file array_info.h + ** \verbatim + ** Original author: lianah + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + /*! \file array_info.h ** \verbatim ** Original author: lianah diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds index 30242db30..2f4bc7313 100644 --- a/src/theory/arrays/kinds +++ b/src/theory/arrays/kinds @@ -5,6 +5,7 @@ # theory THEORY_ARRAY ::CVC4::theory::arrays::TheoryArrays "theory/arrays/theory_arrays.h" +typechecker "theory/arrays/theory_arrays_type_rules.h" properties polite stable-infinite properties check propagate presolve @@ -23,4 +24,7 @@ operator SELECT 2 "array select" # store a i e is a[i] <= e operator STORE 3 "array store" +typerule SELECT ::CVC4::theory::arrays::ArraySelectTypeRule +typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule + endtheory diff --git a/src/theory/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp index 1e135514a..dfa32418f 100644 --- a/src/theory/arrays/static_fact_manager.cpp +++ b/src/theory/arrays/static_fact_manager.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file static_fact_manager.cpp ** \verbatim - ** Original author: mdeters + ** Original author: barrett ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h index de487f97c..5e1ba27a3 100644 --- a/src/theory/arrays/static_fact_manager.h +++ b/src/theory/arrays/static_fact_manager.h @@ -1,11 +1,11 @@ /********************* */ /*! \file static_fact_manager.h ** \verbatim - ** Original author: mdeters + ** Original author: barrett ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index 888a98a45..6985aaea8 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -2,8 +2,8 @@ /*! \file theory_arrays.cpp ** \verbatim ** Original author: barrett - ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -22,6 +22,7 @@ #include "expr/kind.h" #include <map> #include "theory/rewriter.h" +#include "expr/command.h" using namespace std; using namespace CVC4; @@ -689,7 +690,7 @@ void TheoryArrays::appendToDiseqList(TNode of, TNode eq) { * Iterates through the indices of a and stores of b and checks if any new * Row lemmas need to be instantiated. */ -bool TheoryArrays::isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j) { +bool TheoryArrays::isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j) { Assert(a.getType().isArray()); Assert(b.getType().isArray()); @@ -984,7 +985,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) { TNode j = store[1]; TNode c = store[0]; - if( !isRedundandRowLemma(store, c, j, i)){ + if( !isRedundantRowLemma(store, c, j, i)){ //&&!propagateFromRow(store, c, j, i)) { queueRowLemma(store, c, j, i); } @@ -1004,7 +1005,7 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b) { TNode c = store[0]; if ( isNonLinear(c) - &&!isRedundandRowLemma(store, c, j, i)){ + &&!isRedundantRowLemma(store, c, j, i)){ //&&!propagateFromRow(store, c, j, i)) { queueRowLemma(store, c, j, i); } @@ -1066,7 +1067,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { Assert(store.getKind()==kind::STORE); TNode j = store[1]; //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; - if(!isRedundandRowLemma(store, store[0], j, i)) { + if(!isRedundantRowLemma(store, store[0], j, i)) { //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<store<<", "<<store[0]<<", "<<j<<", "<<i<<")\n"; queueRowLemma(store, store[0], j, i); } @@ -1078,7 +1079,7 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a) { Assert(instore.getKind()==kind::STORE); TNode j = instore[1]; //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; - if(!isRedundandRowLemma(instore, instore[0], j, i)) { + if(!isRedundantRowLemma(instore, instore[0], j, i)) { //Trace("arrays-lem")<<"Arrays::checkRowForIndex ("<<instore<<", "<<instore[0]<<", "<<j<<", "<<i<<")\n"; queueRowLemma(instore, instore[0], j, i); } @@ -1104,7 +1105,7 @@ void TheoryArrays::checkStore(TNode a) { for(; it!= js->end(); it++) { TNode j = *it; - if(!isRedundandRowLemma(a, b, i, j)) { + if(!isRedundantRowLemma(a, b, i, j)) { //Trace("arrays-lem")<<"Arrays::checkRowStore ("<<a<<", "<<b<<", "<<i<<", "<<j<<")\n"; queueRowLemma(a,b,i,j); } @@ -1141,7 +1142,17 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) { && d_extAlreadyAdded.count(make_pair(b, a)) == 0) { NodeManager* nm = NodeManager::currentNM(); - Node k = nm->mkVar(a.getType()[0]); + TypeNode ixType = a.getType()[0]; + Node k = nm->mkVar(ixType); + if(Dump.isOn("declarations")) { + stringstream kss; + kss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump("declarations"))) << k; + string ks = kss.str(); + Dump("declarations") + << CommentCommand(ks + " is an extensional lemma index variable " + "from the theory of arrays") << endl + << DeclareFunctionCommand(ks, ixType.toType()) << endl; + } Node eq = nm->mkNode(kind::EQUAL, a, b); Node ak = nm->mkNode(kind::SELECT, a, k); Node bk = nm->mkNode(kind::SELECT, b, k); @@ -1154,7 +1165,7 @@ inline void TheoryArrays::addExtLemma(TNode a, TNode b) { ++d_numExt; return; } - Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; + Trace("arrays-cle")<<"Arrays::checkExtLemmas lemma already generated. \n"; } diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index cf822cb65..37fffd2ec 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -2,10 +2,10 @@ /*! \file theory_arrays.h ** \verbatim ** Original author: mdeters - ** Major contributors: barrett - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing @@ -254,7 +254,7 @@ private: bool isAxiom(TNode lhs, TNode rhs); - bool isRedundandRowLemma(TNode a, TNode b, TNode i, TNode j); + bool isRedundantRowLemma(TNode a, TNode b, TNode i, TNode j); bool isRedundantInContext(TNode a, TNode b, TNode i, TNode j); diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index d7b37d8ba..8c1c16de2 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_arrays_rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: barrett, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp index b0f06b78e..57fd412e4 100644 --- a/src/theory/arrays/union_find.cpp +++ b/src/theory/arrays/union_find.cpp @@ -1,11 +1,11 @@ /********************* */ /*! \file union_find.cpp ** \verbatim - ** Original author: mdeters + ** Original author: lianah ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/arrays/union_find.h b/src/theory/arrays/union_find.h index 4a882806c..7ae85424d 100644 --- a/src/theory/arrays/union_find.h +++ b/src/theory/arrays/union_find.h @@ -1,11 +1,11 @@ /********************* */ /*! \file union_find.h ** \verbatim - ** Original author: mdeters + ** Original author: lianah ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp index fd44ec13b..318fdecce 100644 --- a/src/theory/booleans/circuit_propagator.cpp +++ b/src/theory/booleans/circuit_propagator.cpp @@ -2,7 +2,7 @@ /*! \file circuit_propagator.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -29,11 +29,11 @@ namespace CVC4 { namespace theory { namespace booleans { -void CircuitPropagator::assert(TNode assertion) +void CircuitPropagator::assert(TNode assertion) { if (assertion.getKind() == kind::AND) { for (unsigned i = 0; i < assertion.getNumChildren(); ++ i) { - assert(assertion[i]); + assert(assertion[i]); } } else { // Analyze the assertion for back-edges and all that diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 73a5be0f8..9593f7735 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -2,7 +2,7 @@ /*! \file circuit_propagator.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) @@ -189,20 +189,16 @@ private: bool d_forwardPropagation; /** Whether to perform backward propagation */ bool d_backwardPropagation; - /** Whether to perform expensive propagations */ - bool d_expensivePropagation; public: /** * Construct a new CircuitPropagator with the given atoms and backEdges. */ - CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true, bool enableExpensive = true) : + CircuitPropagator(std::vector<Node>& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) : d_conflict(false), d_learnedLiterals(outLearnedLiterals), d_forwardPropagation(enableForward), - d_backwardPropagation(enableBackward), - d_expensivePropagation(enableExpensive) - { + d_backwardPropagation(enableBackward) { } /** Assert for propagation */ diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds index d540d57f5..5580418e5 100644 --- a/src/theory/booleans/kinds +++ b/src/theory/booleans/kinds @@ -5,6 +5,7 @@ # theory THEORY_BOOL ::CVC4::theory::booleans::TheoryBool "theory/booleans/theory_bool.h" +typechecker "theory/booleans/theory_bool_type_rules.h" properties finite @@ -31,4 +32,14 @@ operator OR 2: "logical or" operator XOR 2 "exclusive or" operator ITE 3 "if-then-else" +typerule CONST_BOOLEAN ::CVC4::theory::boolean::BooleanTypeRule + +typerule NOT ::CVC4::theory::boolean::BooleanTypeRule +typerule AND ::CVC4::theory::boolean::BooleanTypeRule +typerule IFF ::CVC4::theory::boolean::BooleanTypeRule +typerule IMPLIES ::CVC4::theory::boolean::BooleanTypeRule +typerule OR ::CVC4::theory::boolean::BooleanTypeRule +typerule XOR ::CVC4::theory::boolean::BooleanTypeRule +typerule ITE ::CVC4::theory::boolean::IteTypeRule + endtheory diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 01185281a..2be1dac55 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -2,7 +2,7 @@ /*! \file theory_bool.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index ce9938b10..d53337fa7 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -2,8 +2,8 @@ /*! \file theory_bool.h ** \verbatim ** Original author: mdeters - ** Major contributors: taking - ** Minor contributors (to current version): barrett + ** Major contributors: none + ** Minor contributors (to current version): dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index d2693268f..4f41d2fa5 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -2,7 +2,7 @@ /*! \file theory_bool_rewriter.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters, barrett ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h index 4a23249d4..6771f775c 100644 --- a/src/theory/booleans/theory_bool_rewriter.h +++ b/src/theory/booleans/theory_bool_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_bool_rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h index 09030d331..e6c3e0f54 100644 --- a/src/theory/booleans/theory_bool_type_rules.h +++ b/src/theory/booleans/theory_bool_type_rules.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index d170469e0..83a372726 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -36,7 +36,6 @@ # check the theory supports the check() function # propagate the theory supports propagate() (and explain()) # staticLearning the theory supports staticLearning() -# registerTerm the theory supports registerTerm() # notifyRestart the theory supports notifyRestart() # presolve the theory supports presolve() # @@ -59,6 +58,12 @@ # future, so if possible, do not rely on them being called (and # implement them as a no-op). # +# typechecker header +# +# Declare that this theory's typechecker class is defined in the +# given header. (#include'd by the TypeChecker class in the expr +# package.) +# # variable K ["comment"] # # This declares a kind K that has no operator (it's conceptually a @@ -122,6 +127,19 @@ # For consistency, constants taking a non-void payload should # start with "CONST_", but this is not enforced. # +# typerule K typechecker-class +# +# Declares that a (previously-declared) kind K is typechecked by +# the typechecker-class. This class should be defined by the +# header given to the "typechecker" command, above. The +# typechecker-class is used this way by the main TypeChecker code: +# +# typechecker-class::computeType(NodeManager* nm, TNode n, bool check) +# +# It returns TypeNode. It should compute the type of n and return it, +# and if "check" is true, should actually perform type checking instead +# of simply type computation. +# # sort K cardinality [well-founded ground-term header | not-well-founded] ["comment"] # # This creates a kind K that represents a sort (a "type constant"). @@ -217,6 +235,7 @@ # theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h" +typechecker "theory/builtin/theory_builtin_type_rules.h" properties stable-infinite @@ -282,4 +301,9 @@ well-founded TUPLE_TYPE \ "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" +typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule +typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule +typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule +typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule + endtheory diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index 1c779bd79..e955539d5 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 4e62401ff..5c3c70443 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): barrett + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp index b71d66c03..f62140263 100644 --- a/src/theory/builtin/theory_builtin_rewriter.cpp +++ b/src/theory/builtin/theory_builtin_rewriter.cpp @@ -2,7 +2,7 @@ /*! \file theory_builtin_rewriter.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 3bfb7fdc5..ce06b4259 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -5,7 +5,7 @@ ** Major contributors: cconway, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h index 30e4e47ec..ba9d104a1 100644 --- a/src/theory/bv/cd_set_collection.h +++ b/src/theory/bv/cd_set_collection.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file cd_set_collection.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + /* * set_collection.h * diff --git a/src/theory/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp index fa0650506..ee4e9903c 100644 --- a/src/theory/bv/equality_engine.cpp +++ b/src/theory/bv/equality_engine.cpp @@ -2,10 +2,10 @@ /*! \file equality_engine.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h index 31a4bfd27..558fd2b7b 100644 --- a/src/theory/bv/equality_engine.h +++ b/src/theory/bv/equality_engine.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds index d10e32ee0..d502c5ecb 100644 --- a/src/theory/bv/kinds +++ b/src/theory/bv/kinds @@ -5,6 +5,7 @@ # theory THEORY_BV ::CVC4::theory::bv::TheoryBV "theory/bv/theory_bv.h" +typechecker "theory/bv/theory_bv_type_rules.h" properties finite properties check propagate @@ -99,4 +100,47 @@ parameterized BITVECTOR_SIGN_EXTEND BITVECTOR_SIGN_EXTEND_OP 1 "bit-vector sign- parameterized BITVECTOR_ROTATE_LEFT BITVECTOR_ROTATE_LEFT_OP 1 "bit-vector rotate left" parameterized BITVECTOR_ROTATE_RIGHT BITVECTOR_ROTATE_RIGHT_OP 1 "bit-vector rotate right" +typerule CONST_BITVECTOR ::CVC4::theory::bv::BitVectorConstantTypeRule + +typerule BITVECTOR_AND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_OR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_XOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_NOT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_NAND ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_NOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_XNOR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule + +typerule BITVECTOR_COMP ::CVC4::theory::bv::BitVectorCompRule + +typerule BITVECTOR_MULT ::CVC4::theory::bv::BitVectorArithRule +typerule BITVECTOR_PLUS ::CVC4::theory::bv::BitVectorArithRule +typerule BITVECTOR_SUB ::CVC4::theory::bv::BitVectorArithRule +typerule BITVECTOR_NEG ::CVC4::theory::bv::BitVectorArithRule + +typerule BITVECTOR_UDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_UREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_SDIV ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_SREM ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_SMOD ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_SHL ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_LSHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_ASHR ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_ROTATE_LEFT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule +typerule BITVECTOR_ROTATE_RIGHT ::CVC4::theory::bv::BitVectorFixedWidthTypeRule + +typerule BITVECTOR_ULT ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_ULE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_UGT ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_UGE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_SLT ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_SLE ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_SGT ::CVC4::theory::bv::BitVectorPredicateTypeRule +typerule BITVECTOR_SGE ::CVC4::theory::bv::BitVectorPredicateTypeRule + +typerule BITVECTOR_EXTRACT ::CVC4::theory::bv::BitVectorExtractTypeRule +typerule BITVECTOR_CONCAT ::CVC4::theory::bv::BitVectorConcatRule +typerule BITVECTOR_REPEAT ::CVC4::theory::bv::BitVectorRepeatTypeRule +typerule BITVECTOR_ZERO_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule +typerule BITVECTOR_SIGN_EXTEND ::CVC4::theory::bv::BitVectorExtendTypeRule + endtheory diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h index 4fb11f105..9e0b09f2f 100644 --- a/src/theory/bv/slice_manager.h +++ b/src/theory/bv/slice_manager.h @@ -1,3 +1,22 @@ +/********************* */ +/*! \file slice_manager.h + ** \verbatim + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + /* * slice_manager.h * diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 593274281..c1fa692b9 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -2,10 +2,10 @@ /*! \file theory_bv.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index 27fadce0b..5c6797e76 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: dejan - ** Minor contributors (to current version): barrett + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index b66fef0a9..68f75847f 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h index e94388754..b1541fa4a 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_core.h +++ b/src/theory/bv/theory_bv_rewrite_rules_core.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: dejan ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 5bcbdf746..a232ad33b 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -2,7 +2,7 @@ /*! \file theory_bv_rewriter.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index 7af5b4496..20da74ce8 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_bv_rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h index 613df47f3..926ceb767 100644 --- a/src/theory/bv/theory_bv_type_rules.h +++ b/src/theory/bv/theory_bv_type_rules.h @@ -2,10 +2,10 @@ /*! \file theory_bv_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: cconway - ** Minor contributors (to current version): mdeters + ** Major contributors: mdeters, cconway + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index a3135f077..fc4fbf834 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -2,10 +2,10 @@ /*! \file theory_bv_utils.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h index b4ff7e135..14f05d14c 100644 --- a/src/theory/datatypes/datatypes_rewriter.h +++ b/src/theory/datatypes/datatypes_rewriter.h @@ -1,8 +1,8 @@ /********************* */ /*! \file datatypes_rewriter.h ** \verbatim - ** Original author: ajreynol - ** Major contributors: mdeters + ** Original author: mdeters + ** Major contributors: ajreynol ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp index 10ee9bf64..6107e7f2c 100644 --- a/src/theory/datatypes/explanation_manager.cpp +++ b/src/theory/datatypes/explanation_manager.cpp @@ -1,3 +1,22 @@ +/********************* */ +/*! \file explanation_manager.cpp + ** \verbatim + ** Original author: ajreynol + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "theory/datatypes/explanation_manager.h" using namespace std; diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds index 47896b1e0..e90712129 100644 --- a/src/theory/datatypes/kinds +++ b/src/theory/datatypes/kinds @@ -5,6 +5,7 @@ # theory THEORY_DATATYPES ::CVC4::theory::datatypes::TheoryDatatypes "theory/datatypes/theory_datatypes.h" +typechecker "theory/datatypes/theory_datatypes_type_rules.h" properties check presolve @@ -70,4 +71,9 @@ constant ASCRIPTION_TYPE \ "util/ascription_type.h" \ "a type parameter for type ascription" +typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule +typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule +typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule +typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule + endtheory diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 6aed9e9fa..7c474a811 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -2,8 +2,8 @@ /*! \file theory_datatypes.cpp ** \verbatim ** Original author: ajreynol - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 1b9e357ed..d91e9e7f4 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: ajreynol ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index 578de69a2..347bc16b3 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -2,7 +2,7 @@ /*! \file theory_datatypes_type_rules.h ** \verbatim ** Original author: ajreynol - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/datatypes/union_find.cpp b/src/theory/datatypes/union_find.cpp index e56c9f282..eacc4e798 100644 --- a/src/theory/datatypes/union_find.cpp +++ b/src/theory/datatypes/union_find.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/datatypes/union_find.h b/src/theory/datatypes/union_find.h index 31b18e7e9..51d1d85bc 100644 --- a/src/theory/datatypes/union_find.h +++ b/src/theory/datatypes/union_find.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: ajreynol ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index d8a54b1e4..0796f3cb0 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/mkrewriter b/src/theory/mkrewriter index ec659d0bb..395317045 100755 --- a/src/theory/mkrewriter +++ b/src/theory/mkrewriter @@ -94,6 +94,18 @@ function endtheory { seen_endtheory=true } +function typechecker { + # typechecker header + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function typerule { + # typerule OPERATOR typechecking-class + lineno=${BASH_LINENO[0]} + check_theory_seen +} + function rewriter { # rewriter class header class="$1" diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits index 538ffb25f..852b29711 100755 --- a/src/theory/mktheorytraits +++ b/src/theory/mktheorytraits @@ -43,7 +43,6 @@ theory_for_each_macro="#define CVC4_FOR_EACH_THEORY \\ theory_has_check="false" theory_has_propagate="false" theory_has_staticLearning="false" -theory_has_registerTerm="false" theory_has_notifyRestart="false" theory_has_presolve="false" @@ -130,7 +129,6 @@ struct TheoryTraits<${theory_id}> { static const bool hasCheck = ${theory_has_check}; static const bool hasPropagate = ${theory_has_propagate}; static const bool hasStaticLearning = ${theory_has_staticLearning}; - static const bool hasRegisterTerm = ${theory_has_registerTerm}; static const bool hasNotifyRestart = ${theory_has_notifyRestart}; static const bool hasPresolve = ${theory_has_presolve}; };/* struct TheoryTraits<${theory_id}> */ @@ -139,7 +137,7 @@ struct TheoryTraits<${theory_id}> { # warnings about theory content and properties dir="$(dirname "$kf")/../../" if [ -e "$dir/$theory_header" ]; then - for function in check propagate staticLearning registerTerm notifyRestart presolve; do + for function in check propagate staticLearning notifyRestart presolve; do if eval "\$theory_has_$function"; then grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' || echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2 @@ -155,7 +153,6 @@ struct TheoryTraits<${theory_id}> { theory_has_check="false" theory_has_propagate="false" theory_has_staticLearning="false" - theory_has_registerTerm="false" theory_has_notifyRestart="false" theory_has_presolve="false" @@ -172,6 +169,17 @@ struct TheoryTraits<${theory_id}> { lineno=${BASH_LINENO[0]} } +function typechecker { + # typechecker header + lineno=${BASH_LINENO[0]} + check_theory_seen +} + +function typerule { + # typerule OPERATOR typechecking-class + lineno=${BASH_LINENO[0]} + check_theory_seen +} function properties { # properties property* @@ -188,7 +196,6 @@ function properties { propagate) theory_has_propagate="true";; staticLearning) theory_has_staticLearning="true";; presolve) theory_has_presolve="true";; - registerTerm) theory_has_registerTerm="true";; notifyRestart) theory_has_notifyRestart="true";; *) echo "$kf:$lineno: error: unknown theory property \"$property\"" >&2; exit 1;; esac diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index d82e628c1..bf928cb62 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -2,10 +2,10 @@ /*! \file output_channel.h ** \verbatim ** Original author: mdeters - ** Major contributors: taking - ** Minor contributors (to current version): barrett + ** Major contributors: none + ** Minor contributors (to current version): taking, barrett ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index bb42a5ec7..f6aa75bbd 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -2,7 +2,7 @@ /*! \file rewriter.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h index 884d0af72..f1a0e2b30 100644 --- a/src/theory/rewriter.h +++ b/src/theory/rewriter.h @@ -2,7 +2,7 @@ /*! \file rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/rewriter_attributes.h b/src/theory/rewriter_attributes.h index a2b2d06b7..c958abb68 100644 --- a/src/theory/rewriter_attributes.h +++ b/src/theory/rewriter_attributes.h @@ -2,7 +2,7 @@ /*! \file rewriter_attributes.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index cbbff95c1..34204ec2d 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -2,7 +2,7 @@ /*! \file rewriter_tables_template.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/shared_data.cpp b/src/theory/shared_data.cpp index 50e916832..3e89dec7e 100644 --- a/src/theory/shared_data.cpp +++ b/src/theory/shared_data.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/shared_data.h b/src/theory/shared_data.h index 181508c54..7d6a9ebd2 100644 --- a/src/theory/shared_data.h +++ b/src/theory/shared_data.h @@ -2,10 +2,10 @@ /*! \file shared_data.h ** \verbatim ** Original author: barrett - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/shared_term_manager.cpp b/src/theory/shared_term_manager.cpp index 03afa984e..20f7a82f1 100644 --- a/src/theory/shared_term_manager.cpp +++ b/src/theory/shared_term_manager.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: barrett ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/shared_term_manager.h b/src/theory/shared_term_manager.h index 7263ac93a..faea8d687 100644 --- a/src/theory/shared_term_manager.h +++ b/src/theory/shared_term_manager.h @@ -2,10 +2,10 @@ /*! \file shared_term_manager.h ** \verbatim ** Original author: barrett - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/substitutions.cpp b/src/theory/substitutions.cpp index 76551bc18..88e5b3dba 100644 --- a/src/theory/substitutions.cpp +++ b/src/theory/substitutions.cpp @@ -1,7 +1,7 @@ /********************* */ /*! \file substitutions.cpp ** \verbatim - ** Original author: mdeters + ** Original author: dejan ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. diff --git a/src/theory/substitutions.h b/src/theory/substitutions.h index f59c17dc0..849c8f166 100644 --- a/src/theory/substitutions.h +++ b/src/theory/substitutions.h @@ -2,7 +2,7 @@ /*! \file substitutions.h ** \verbatim ** Original author: mdeters - ** Major contributors: none + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 576e0188b..b772d9d23 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -5,7 +5,7 @@ ** Major contributors: taking ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/theory.h b/src/theory/theory.h index 62a8cb4d6..a1d62ca04 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "expr/attribute.h" +#include "expr/command.h" #include "theory/valuation.h" #include "theory/substitutions.h" #include "theory/output_channel.h" @@ -125,10 +126,9 @@ protected: Valuation d_valuation; /** - * Returns the next atom in the assertFact() queue. Guarantees that - * registerTerm() has been called on the theory specific subterms. + * Returns the next atom in the assertFact() queue. * - * @return the next atom in the assertFact() queue. + * @return the next atom in the assertFact() queue */ TNode get() { Assert( !done(), "Theory::get() called with assertion queue empty!" ); @@ -136,7 +136,11 @@ protected: d_wasSharedTermFact = false; d_factsHead = d_factsHead + 1; Trace("theory") << "Theory::get() => " << fact - << " (" << d_facts.size() - d_factsHead << " left)" << std::endl; + << " (" << d_facts.size() - d_factsHead << " left)" + << std::endl; + if(Dump.isOn("state")) { + Dump("state") << AssertCommand(fact.toExpr()) << std::endl; + } return fact; } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e604c45df..040582c9f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -2,8 +2,8 @@ /*! \file theory_engine.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: taking, barrett, dejan - ** Minor contributors (to current version): cconway + ** Major contributors: barrett, dejan + ** Minor contributors (to current version): cconway, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -37,18 +37,18 @@ using namespace std; using namespace CVC4; using namespace CVC4::theory; -/** Tag for the "preregisterTerm()-has-benn-called" flag on nodes */ -struct PreRegisteredAttrTag {}; -/** The "preregisterTerm()-has-been-called" flag on Nodes */ -typedef expr::Attribute<PreRegisteredAttrTag, Theory::Set> PreRegisteredAttr; - TheoryEngine::TheoryEngine(context::Context* ctxt) : d_propEngine(NULL), d_context(ctxt), d_activeTheories(0), + d_atomPreprocessingCache(), + d_possiblePropagations(), + d_hasPropagated(ctxt), d_theoryOut(this, ctxt), + d_sharedTermManager(NULL), d_hasShutDown(false), d_incomplete(ctxt, false), + d_logic(""), d_statistics(), d_preRegistrationVisitor(*this, ctxt) { @@ -87,6 +87,10 @@ struct preregister_stack_element { };/* struct preprocess_stack_element */ void TheoryEngine::preRegister(TNode preprocessed) { + if(Dump.isOn("missed-t-propagations")) { + d_possiblePropagations.push_back(preprocessed); + } + NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed); } @@ -112,8 +116,14 @@ void TheoryEngine::check(theory::Theory::Effort effort) { // Do the checking try { CVC4_FOR_EACH_THEORY; + + if(Dump.isOn("missed-t-conflicts")) { + Dump("missed-t-conflicts") + << CommentCommand("Completeness check for T-conflicts; expect sat") << endl + << CheckSatCommand() << endl; + } } catch(const theory::Interrupted&) { - Trace("theory") << "TheoryEngine::check() => conflict" << std::endl; + Trace("theory") << "TheoryEngine::check() => conflict" << endl; } } @@ -124,11 +134,54 @@ void TheoryEngine::propagate() { #endif #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits<THEORY>::hasPropagate && isActive(THEORY)) { \ - reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ + reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->propagate(theory::Theory::FULL_EFFORT); \ } // Propagate for each theory using the statement above CVC4_FOR_EACH_THEORY; + + if(Dump.isOn("missed-t-propagations")) { + for(vector<TNode>::iterator i = d_possiblePropagations.begin(); + i != d_possiblePropagations.end(); + ++i) { + if(d_hasPropagated.find(*i) == d_hasPropagated.end()) { + Dump("missed-t-propagations") + << CommentCommand("Completeness check for T-propagations; expect invalid") << endl + << QueryCommand((*i).toExpr()) << endl; + } + } + } +} + +Node TheoryEngine::getExplanation(TNode node, theory::Theory* theory) { + theory->explain(node); + if(Dump.isOn("t-explanations")) { + Dump("t-explanations") + << CommentCommand(string("theory explanation from ") + + theory->identify() + ": expect valid") << endl + << QueryCommand(d_theoryOut.d_explanationNode.get().impNode(node).toExpr()) + << endl; + } + Assert(properExplanation(node, d_theoryOut.d_explanationNode.get())); + return d_theoryOut.d_explanationNode; +} + +bool TheoryEngine::properConflict(TNode conflict) const { + Assert(!conflict.isNull()); +#warning fixme + return true; +} + +bool TheoryEngine::properPropagation(TNode lit) const { + Assert(!lit.isNull()); +#warning fixme + return true; +} + +bool TheoryEngine::properExplanation(TNode node, TNode expl) const { + Assert(!node.isNull() && !expl.isNull()); +#warning fixme + return true; } Node TheoryEngine::getValue(TNode node) { @@ -212,11 +265,27 @@ void TheoryEngine::staticLearning(TNode in, NodeBuilder<>& learned) { CVC4_FOR_EACH_THEORY; } +void TheoryEngine::shutdown() { + // Set this first; if a Theory shutdown() throws an exception, + // at least the destruction of the TheoryEngine won't confound + // matters. + d_hasShutDown = true; + + // Shutdown all the theories + for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { + if(d_theoryTable[theoryId]) { + d_theoryTable[theoryId]->shutdown(); + } + } + + theory::Rewriter::shutdown(); +} + theory::Theory::SolveStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitionOut) { TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal; - Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << std::endl; + Trace("theory") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl; Theory::SolveStatus solveStatus = theoryOf(atom)->solve(literal, substitionOut); - Trace("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << std::endl; + Trace("theory") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl; return solveStatus; } @@ -230,9 +299,9 @@ struct preprocess_stack_element { Node TheoryEngine::preprocess(TNode assertion) { - Trace("theory") << "TheoryEngine::preprocess(" << assertion << ")" << std::endl; + Trace("theory") << "TheoryEngine::preprocess(" << assertion << ")" << endl; - // Do a topological sort of the subexpressions and substitute them + // Do a topological sort of the subexpressions and substitute them vector<preprocess_stack_element> toVisit; toVisit.push_back(assertion); @@ -242,7 +311,7 @@ Node TheoryEngine::preprocess(TNode assertion) { preprocess_stack_element& stackHead = toVisit.back(); TNode current = stackHead.node; - Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << std::endl; + Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): processing " << current << endl; // If node already in the cache we're done, pop from the stack NodeMap::iterator find = d_atomPreprocessingCache.find(current); @@ -270,7 +339,7 @@ Node TheoryEngine::preprocess(TNode assertion) { } // Mark the substitution and continue Node result = builder; - Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << std::endl; + Debug("theory::internal") << "TheoryEngine::preprocess(" << assertion << "): setting " << current << " -> " << result << endl; d_atomPreprocessingCache[current] = result; toVisit.pop_back(); } else { @@ -287,7 +356,7 @@ Node TheoryEngine::preprocess(TNode assertion) { } } else { // No children, so we're done - Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << std::endl; + Debug("substitution::internal") << "SubstitutionMap::internalSubstitute(" << assertion << "): setting " << current << " -> " << current << endl; d_atomPreprocessingCache[current] = current; toVisit.pop_back(); } diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2107bcb66..815a79a5a 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -2,8 +2,8 @@ /*! \file theory_engine.h ** \verbatim ** Original author: mdeters - ** Major contributors: taking, dejan - ** Minor contributors (to current version): cconway, barrett + ** Major contributors: dejan + ** Minor contributors (to current version): cconway, barrett, taking ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -26,7 +26,9 @@ #include <utility> #include "expr/node.h" +#include "expr/command.h" #include "prop/prop_engine.h" +#include "context/cdset.h" #include "theory/shared_term_manager.h" #include "theory/theory.h" #include "theory/substitutions.h" @@ -77,6 +79,19 @@ class TheoryEngine { NodeMap d_atomPreprocessingCache; /** + * Used for "missed-t-propagations" dumping mode only. A set of all + * theory-propagable literals. + */ + std::vector<TNode> d_possiblePropagations; + + /** + * Used for "missed-t-propagations" dumping mode only. A + * context-dependent set of those theory-propagable literals that + * have been propagated. + */ + context::CDSet<TNode, TNodeHashFunction> d_hasPropagated; + + /** * An output channel for Theory that passes messages * back to a TheoryEngine. */ @@ -122,13 +137,16 @@ class TheoryEngine { d_explanationNode(context) { } - void newFact(TNode n); - void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) { Trace("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl; d_inConflict = true; + if(Dump.isOn("t-conflicts")) { + Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat") << std::endl + << CheckSatCommand(conflictNode.toExpr()) << std::endl; + } + Assert(d_engine->properConflict(conflictNode)); ++(d_engine->d_statistics.d_statConflicts); // Construct the lemma (note that no CNF caching should happen as all the literals already exists) @@ -144,6 +162,15 @@ class TheoryEngine { throw(theory::Interrupted, AssertionException) { Trace("theory") << "EngineOutputChannel::propagate(" << lit << ")" << std::endl; + if(Dump.isOn("t-propagations")) { + Dump("t-propagations") + << CommentCommand("negation of theory propagation: expect valid") << std::endl + << QueryCommand(lit.toExpr()) << std::endl; + } + if(Dump.isOn("missed-t-propagations")) { + d_engine->d_hasPropagated.insert(lit); + } + Assert(d_engine->properPropagation(lit)); d_propagatedLiterals.push_back(lit); ++(d_engine->d_statistics.d_statPropagate); } @@ -152,6 +179,10 @@ class TheoryEngine { throw(theory::Interrupted, TypeCheckingExceptionPrivate, AssertionException) { Trace("theory") << "EngineOutputChannel::lemma(" << node << ")" << std::endl; + if(Dump.isOn("t-lemmas")) { + Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") << std::endl + << QueryCommand(node.toExpr()) << std::endl; + } ++(d_engine->d_statistics.d_statLemma); d_engine->newLemma(node, false, removable); @@ -161,12 +192,12 @@ class TheoryEngine { throw(theory::Interrupted, AssertionException) { Trace("theory") << "EngineOutputChannel::explanation(" << explanationNode << ")" << std::endl; + // handle dumping of explanations elsewhere.. d_explanationNode = explanationNode; ++(d_engine->d_statistics.d_statExplanation); } - void setIncomplete() - throw(theory::Interrupted, AssertionException) { + void setIncomplete() throw(theory::Interrupted, AssertionException) { d_engine->d_incomplete = true; } };/* class EngineOutputChannel */ @@ -177,12 +208,6 @@ class TheoryEngine { SharedTermManager* d_sharedTermManager; /** - * Whether or not theory registration is on. May not be safe to - * turn off with some theories. - */ - bool d_theoryRegistration; - - /** * Debugging flag to ensure that shutdown() is called before the * destructor. */ @@ -224,14 +249,15 @@ public: * there is another theory it will be deleted. */ template <class TheoryClass> - void addTheory() { + inline void addTheory() { TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this)); d_theoryTable[theory->getId()] = theory; d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory)); } /** - * Set's the logic (smt-lib format). All theory specific setup/hacks should go in here. + * Sets the logic (SMT-LIB format). All theory specific setup/hacks + * should go in here. */ void setLogic(std::string logic); @@ -239,7 +265,7 @@ public: return d_sharedTermManager; } - void setPropEngine(prop::PropEngine* propEngine) { + inline void setPropEngine(prop::PropEngine* propEngine) { Assert(d_propEngine == NULL); d_propEngine = propEngine; } @@ -247,7 +273,7 @@ public: /** * Get a pointer to the underlying propositional engine. */ - prop::PropEngine* getPropEngine() const { + inline prop::PropEngine* getPropEngine() const { return d_propEngine; } @@ -260,7 +286,7 @@ public: /** * Return whether or not we are incomplete (in the current context). */ - bool isIncomplete() { + inline bool isIncomplete() { return d_incomplete; } @@ -269,21 +295,7 @@ public: * destruction. It is important because there are destruction * ordering issues between PropEngine and Theory. */ - void shutdown() { - // Set this first; if a Theory shutdown() throws an exception, - // at least the destruction of the TheoryEngine won't confound - // matters. - d_hasShutDown = true; - - // Shutdown all the theories - for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) { - if(d_theoryTable[theoryId]) { - d_theoryTable[theoryId]->shutdown(); - } - } - - theory::Rewriter::shutdown(); - } + void shutdown(); /** * Get the theory associated to a given Node. @@ -367,7 +379,7 @@ public: return d_theoryOut.d_propagatedLiterals; } - void clearPropagatedLiterals() { + inline void clearPropagatedLiterals() { d_theoryOut.d_propagatedLiterals.clear(); } @@ -384,16 +396,25 @@ public: void propagate(); - inline Node getExplanation(TNode node, theory::Theory* theory) { - theory->explain(node); - return d_theoryOut.d_explanationNode; - } + Node getExplanation(TNode node, theory::Theory* theory); + + bool properConflict(TNode conflict) const; + bool properPropagation(TNode lit) const; + bool properExplanation(TNode node, TNode expl) const; inline Node getExplanation(TNode node) { d_theoryOut.d_explanationNode = Node::null(); TNode atom = node.getKind() == kind::NOT ? node[0] : node; theoryOf(atom)->explain(node); Assert(!d_theoryOut.d_explanationNode.get().isNull()); + if(Dump.isOn("t-explanations")) { + Dump("t-explanations") + << CommentCommand(std::string("theory explanation from ") + + theoryOf(atom)->identify() + ": expect valid") << std::endl + << QueryCommand(d_theoryOut.d_explanationNode.get().impNode(node).toExpr()) + << std::endl; + } + Assert(properExplanation(node, d_theoryOut.d_explanationNode.get())); return d_theoryOut.d_explanationNode; } diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index 0b377fb11..ec2405295 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -5,7 +5,7 @@ ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index 525c06b3c..bbf13b425 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -2,7 +2,7 @@ /*! \file theory_traits_template.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index fc0f32927..f25e50ec9 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -5,10 +5,6 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libuf.la -# force automake to link using g++ -nodist_EXTRA_libuf_la_SOURCES = \ - dummy.cpp - libuf_la_SOURCES = \ theory_uf.h \ theory_uf.cpp \ @@ -19,10 +15,4 @@ libuf_la_SOURCES = \ symmetry_breaker.h \ symmetry_breaker.cpp -libuf_la_LIBADD = \ - @builddir@/tim/libuftim.la \ - @builddir@/morgan/libufmorgan.la - -SUBDIRS = tim morgan - EXTRA_DIST = kinds diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 4f3879560..ba607526f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h index 1dd9963f7..bea6ff9a9 100644 --- a/src/theory/uf/equality_engine_impl.h +++ b/src/theory/uf/equality_engine_impl.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 6cec23385..1f8643330 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -5,11 +5,14 @@ # theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h" +typechecker "theory/uf/theory_uf_type_rules.h" properties stable-infinite -properties check propagate staticLearning presolve notifyRestart +properties check propagate staticLearning presolve rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h" parameterized APPLY_UF VARIABLE 1: "uninterpreted function application" +typerule APPLY_UF ::CVC4::theory::uf::UfTypeRule + endtheory diff --git a/src/theory/uf/morgan/Makefile b/src/theory/uf/morgan/Makefile deleted file mode 100644 index 4f6767bdd..000000000 --- a/src/theory/uf/morgan/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../../.. -srcdir = src/theory/uf/morgan - -include $(topdir)/Makefile.subdir diff --git a/src/theory/uf/morgan/Makefile.am b/src/theory/uf/morgan/Makefile.am deleted file mode 100644 index 886178a6f..000000000 --- a/src/theory/uf/morgan/Makefile.am +++ /dev/null @@ -1,16 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libufmorgan.la - -libufmorgan_la_SOURCES = \ - theory_uf_morgan.h \ - theory_uf_morgan.cpp \ - union_find.h \ - union_find.cpp \ - stacking_map.h \ - stacking_map.cpp - -EXTRA_DIST = diff --git a/src/theory/uf/morgan/stacking_map.cpp b/src/theory/uf/morgan/stacking_map.cpp deleted file mode 100644 index 16a85e71b..000000000 --- a/src/theory/uf/morgan/stacking_map.cpp +++ /dev/null @@ -1,83 +0,0 @@ -/********************* */ -/*! \file stacking_map.cpp - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Backtrackable map using an undo stack - ** - ** Backtrackable map using an undo stack rather than storing items in - ** a CDMap<>. - **/ - -#include <iostream> - -#include "theory/uf/morgan/stacking_map.h" -#include "util/Assert.h" -#include "expr/node.h" - -using namespace std; - -namespace CVC4 { -namespace theory { -namespace uf { -namespace morgan { - -template <class NodeType, class NodeHash> -TNode StackingMap<NodeType, NodeHash>::find(TNode n) const { - typename MapType::const_iterator i = d_map.find(n); - if(i == d_map.end()) { - return TNode(); - } else { - return (*i).second; - } -} - -template <class NodeType, class NodeHash> -void StackingMap<NodeType, NodeHash>::set(TNode n, TNode newValue) { - Trace("ufsm") << "UFSM setting " << n << " : " << newValue << " @ " << d_trace.size() << endl; - NodeType& ref = d_map[n]; - d_trace.push_back(make_pair(n, TNode(ref))); - d_offset = d_trace.size(); - ref = newValue; -} - -template <class NodeType, class NodeHash> -void StackingMap<NodeType, NodeHash>::notify() { - Trace("ufsm") << "UFSM cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; - while(d_offset < d_trace.size()) { - pair<TNode, TNode> p = d_trace.back(); - if(p.second.isNull()) { - d_map.erase(p.first); - Trace("ufsm") << "UFSM " << d_trace.size() << " erasing " << p.first << endl; - } else { - d_map[p.first] = p.second; - Trace("ufsm") << "UFSM " << d_trace.size() << " replacing " << p << endl; - } - d_trace.pop_back(); - } - Trace("ufufsm") << "UFSM cancelling finished." << endl; -} - -// The following declarations allow us to put functions in the .cpp file -// instead of the header, since we know which instantiations are needed. - -template TNode StackingMap<Node, NodeHashFunction>::find(TNode n) const; -template void StackingMap<Node, NodeHashFunction>::set(TNode n, TNode newValue); -template void StackingMap<Node, NodeHashFunction>::notify(); - -template TNode StackingMap<TNode, TNodeHashFunction>::find(TNode n) const; -template void StackingMap<TNode, TNodeHashFunction>::set(TNode n, TNode newValue); -template void StackingMap<TNode, TNodeHashFunction>::notify(); - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/uf/morgan/stacking_map.h b/src/theory/uf/morgan/stacking_map.h deleted file mode 100644 index c54acc363..000000000 --- a/src/theory/uf/morgan/stacking_map.h +++ /dev/null @@ -1,91 +0,0 @@ -/********************* */ -/*! \file stacking_map.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Backtrackable map using an undo stack - ** - ** Backtrackable map using an undo stack rather than storing items in - ** a CDMap<>. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__MORGAN__STACKING_MAP_H -#define __CVC4__THEORY__UF__MORGAN__STACKING_MAP_H - -#include <utility> -#include <vector> -#include <ext/hash_map> - -#include "expr/node.h" -#include "context/cdo.h" - -namespace CVC4 { - -namespace context { - class Context; -}/* CVC4::context namespace */ - -namespace theory { -namespace uf { -namespace morgan { - -// NodeType \in { Node, TNode } -template <class NodeType, class NodeHash> -class StackingMap : context::ContextNotifyObj { - /** Our underlying map type. */ - typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType; - - /** - * Our map of Nodes to their values. - */ - MapType d_map; - - /** Our undo stack for changes made to d_map. */ - std::vector<std::pair<TNode, TNode> > d_trace; - - /** Our current offset in the d_trace stack (context-dependent). */ - context::CDO<size_t> d_offset; - -public: - StackingMap(context::Context* ctxt) : - context::ContextNotifyObj(ctxt), - d_offset(ctxt, 0) { - } - - ~StackingMap() throw() { } - - /** - * Return a Node's value in the key-value map. If n is not a key in - * the map, this function returns TNode::null(). - */ - TNode find(TNode n) const; - - /** - * Set the value in the key-value map for Node n to newValue. - */ - void set(TNode n, TNode newValue); - - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::notify(). - */ - void notify(); - -};/* class StackingMap<> */ - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /*__CVC4__THEORY__UF__MORGAN__STACKING_MAP_H */ diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp deleted file mode 100644 index 01bab53ac..000000000 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ /dev/null @@ -1,751 +0,0 @@ -/********************* */ -/*! \file theory_uf_morgan.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of the theory of uninterpreted functions. - ** - ** Implementation of the theory of uninterpreted functions. - **/ - -#include "theory/uf/morgan/theory_uf_morgan.h" -#include "theory/valuation.h" -#include "expr/kind.h" -#include "util/congruence_closure.h" -#include "theory/uf/symmetry_breaker.h" - -#include <map> - -using namespace std; - -using namespace CVC4; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; -using namespace CVC4::theory::uf::morgan; - -TheoryUFMorgan::TheoryUFMorgan(Context* ctxt, OutputChannel& out, Valuation valuation) : - TheoryUF(ctxt, out, valuation), - d_assertions(ctxt), - d_ccChannel(this), - d_cc(ctxt, &d_ccChannel), - d_unionFind(ctxt), - d_disequalities(ctxt), - d_equalities(ctxt), - d_conflict(), - d_trueNode(), - d_falseNode(), - d_trueEqFalseNode(), - d_ccExplanationLength("theory::uf::morgan::cc::averageExplanationLength", - d_cc.getExplanationLength()), - d_ccNewSkolemVars("theory::uf::morgan::cc::newSkolemVariables", - d_cc.getNewSkolemVars()) { - - StatisticsRegistry::registerStat(&d_ccExplanationLength); - StatisticsRegistry::registerStat(&d_ccNewSkolemVars); - - NodeManager* nm = NodeManager::currentNM(); - TypeNode boolType = nm->booleanType(); - d_trueNode = nm->mkVar("TRUE_UF", boolType); - d_falseNode = nm->mkVar("FALSE_UF", boolType); - d_trueEqFalseNode = nm->mkNode(kind::IFF, d_trueNode, d_falseNode); - addDisequality(d_trueEqFalseNode); - d_cc.addTerm(d_trueNode); - d_cc.addTerm(d_falseNode); -} - -TheoryUFMorgan::~TheoryUFMorgan() { - d_trueNode = Node::null(); - d_falseNode = Node::null(); - d_trueEqFalseNode = Node::null(); - - StatisticsRegistry::unregisterStat(&d_ccExplanationLength); - StatisticsRegistry::unregisterStat(&d_ccNewSkolemVars); -} - -void TheoryUFMorgan::preRegisterTerm(TNode n) { - Debug("uf") << "uf: preRegisterTerm(" << n << ")" << endl; - if(n.getKind() == kind::EQUAL || n.getKind() == kind::IFF) { - registerEqualityForPropagation(n); - } -} - -void TheoryUFMorgan::registerTerm(TNode n) { - Debug("uf") << "uf: registerTerm(" << n << ")" << endl; -} - -Node TheoryUFMorgan::constructConflict(TNode diseq) { - Debug("uf") << "uf: begin constructConflict()" << endl; - Debug("uf") << "uf: using diseq == " << diseq << endl; - - Node explanation = d_cc.explain(diseq[0], diseq[1]); - - NodeBuilder<> nb(kind::AND); - if(explanation.getKind() == kind::AND) { - for(TNode::iterator i = TNode(explanation).begin(); - i != TNode(explanation).end(); - ++i) { - TNode n = *i; - Assert(n.getKind() == kind::EQUAL || - n.getKind() == kind::IFF); - Assert(n[0] != d_trueNode && - n[0] != d_falseNode); - if(n[1] == d_trueNode) { - nb << n[0]; - } else if(n[1] == d_falseNode) { - nb << n[0].notNode(); - } else { - nb << n; - } - } - } else { - Assert(explanation.getKind() == kind::EQUAL || - explanation.getKind() == kind::IFF); - Assert(explanation[0] != d_trueNode && - explanation[0] != d_falseNode); - if(explanation[1] == d_trueNode) { - nb << explanation[0]; - } else if(explanation[1] == d_falseNode) { - nb << explanation[0].notNode(); - } else { - nb << explanation; - } - } - if(diseq != d_trueEqFalseNode) { - nb << diseq.notNode(); - } - - // by construction this should be true - Assert(nb.getNumChildren() > 1); - - Node conflict = nb; - Debug("uf") << "conflict constructed : " << conflict << endl; - - Debug("uf") << "uf: ending constructConflict()" << endl; - - return conflict; -} - -void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) { - Debug("uf") << "uf: notified of merge " << a << endl - << " and " << b << endl; - if(!d_conflict.isNull()) { - // if already a conflict, we don't care - return; - } - - merge(a, b); -} - -void TheoryUFMorgan::merge(TNode a, TNode b) { - Assert(d_conflict.isNull()); - - // make "a" the one with shorter diseqList - EqLists::iterator deq_ia = d_disequalities.find(a); - EqLists::iterator deq_ib = d_disequalities.find(b); - if(deq_ia != d_disequalities.end()) { - if(deq_ib == d_disequalities.end() || - (*deq_ia).second->size() > (*deq_ib).second->size()) { - TNode tmp = a; - a = b; - b = tmp; - Debug("uf") << " swapping to make a shorter diseqList" << endl; - } - } - a = find(a); - b = find(b); - Debug("uf") << "uf: uf reps are " << a << endl - << " and " << b << endl; - - if(a == b) { - return; - } - - // should have already found such a conflict - Assert(find(d_trueNode) != find(d_falseNode)); - - d_unionFind.setCanon(a, b); - - EqLists::iterator deq_i = d_disequalities.find(a); - // a set of other trees we are already disequal to, and their - // (TNode) equalities (for optimizations below) - map<TNode, TNode> alreadyDiseqs; - if(deq_i != d_disequalities.end()) { - EqLists::iterator deq_ib = d_disequalities.find(b); - if(deq_ib != d_disequalities.end()) { - EqList* deq = (*deq_ib).second; - for(EqList::const_iterator j = deq->begin(); j != deq->end(); ++j) { - TNode deqn = *j; - TNode s = deqn[0]; - TNode t = deqn[1]; - TNode sp = find(s); - TNode tp = find(t); - Assert(sp == b || tp == b); - if(sp == b) { - alreadyDiseqs[tp] = deqn; - } else { - alreadyDiseqs[sp] = deqn; - } - } - } - - EqList* deq = (*deq_i).second; - if(Debug.isOn("uf")) { - Debug("uf") << "a == " << a << endl; - Debug("uf") << "size of deq(a) is " << deq->size() << endl; - } - for(EqList::const_iterator j = deq->begin(); j != deq->end(); ++j) { - Debug("uf") << " deq(a) ==> " << *j << endl; - TNode deqn = *j; - Assert(deqn.getKind() == kind::EQUAL || - deqn.getKind() == kind::IFF); - TNode s = deqn[0]; - TNode t = deqn[1]; - if(Debug.isOn("uf")) { - Debug("uf") << " s ==> " << s << endl - << " t ==> " << t << endl - << " find(s) ==> " << debugFind(s) << endl - << " find(t) ==> " << debugFind(t) << endl; - } - TNode sp = find(s); - TNode tp = find(t); - if(sp == tp) { - d_conflict = deqn; - return; - } - Assert(sp == b || tp == b); - // optimization: don't put redundant diseq's in the list - if(sp == b) { - if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[tp] = deqn; - } - } else { - if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) { - appendToDiseqList(b, deqn); - alreadyDiseqs[sp] = deqn; - } - } - } - Debug("uf") << "end diseq-list." << endl; - } - - // Note that at this point, alreadyDiseqs contains everything we're - // disequal to, and the attendant disequality - - // FIXME these could be "remembered" and then done in propagation (?) -// EqLists::iterator eq_i = d_equalities.find(a); -// if(eq_i != d_equalities.end()) { -// EqList* eq = (*eq_i).second; -// if(Debug.isOn("uf")) { -// Debug("uf") << "a == " << a << endl; -// Debug("uf") << "size of eq(a) is " << eq->size() << endl; -// } -// for(EqList::const_iterator j = eq->begin(); j != eq->end(); ++j) { -// Debug("uf") << " eq(a) ==> " << *j << endl; -// TNode eqn = *j; -// Assert(eqn.getKind() == kind::EQUAL || -// eqn.getKind() == kind::IFF); -// TNode s = eqn[0]; -// TNode t = eqn[1]; -// if(Debug.isOn("uf")) { -// Debug("uf") << " s ==> " << s << endl -// << " t ==> " << t << endl -// << " find(s) ==> " << debugFind(s) << endl -// << " find(t) ==> " << debugFind(t) << endl; -// } -// TNode sp = find(s); -// TNode tp = find(t); -// if(sp == tp) { -// // propagation of equality -// Debug("uf:prop") << " uf-propagating " << eqn << endl; -// ++d_propagations; -// d_out->propagate(eqn); -// } else { -// Assert(sp == b || tp == b); -// appendToEqList(b, eqn); -// if(sp == b) { -// map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(tp); -// if(k != alreadyDiseqs.end()) { -// // propagation of disequality -// // FIXME: this will propagate the same disequality on every -// // subsequent merge, won't it?? -// Node deqn = (*k).second.notNode(); -// Debug("uf:prop") << " uf-propagating " << deqn << endl; -// ++d_propagations; -// d_out->propagate(deqn); -// } -// } else { -// map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(sp); -// if(k != alreadyDiseqs.end()) { -// // propagation of disequality -// // FIXME: this will propagate the same disequality on every -// // subsequent merge, won't it?? -// Node deqn = (*k).second.notNode(); -// Debug("uf:prop") << " uf-propagating " << deqn << endl; -// ++d_propagations; -// d_out->propagate(deqn); -// } -// } -// } -// } -// Debug("uf") << "end eq-list." << endl; -// } -} - -void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) { - Debug("uf") << "appending " << eq << endl - << " to diseq list of " << of << endl; - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - Assert(of == debugFind(of)); - EqLists::iterator deq_i = d_disequalities.find(of); - EqList* deq; - if(deq_i == d_disequalities.end()) { - deq = new(getContext()->getCMM()) EqList(true, getContext(), false, - ContextMemoryAllocator<TNode>(getContext()->getCMM())); - d_disequalities.insertDataFromContextMemory(of, deq); - } else { - deq = (*deq_i).second; - } - deq->push_back(eq); - if(Debug.isOn("uf")) { - Debug("uf") << " size is now " << deq->size() << endl; - } -} - -void TheoryUFMorgan::appendToEqList(TNode of, TNode eq) { - Debug("uf") << "appending " << eq << endl - << " to eq list of " << of << endl; - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - Assert(of == debugFind(of)); - EqLists::iterator eq_i = d_equalities.find(of); - EqList* eql; - if(eq_i == d_equalities.end()) { - eql = new(getContext()->getCMM()) EqList(true, getContext(), false, - ContextMemoryAllocator<TNode>(getContext()->getCMM())); - d_equalities.insertDataFromContextMemory(of, eql); - } else { - eql = (*eq_i).second; - } - eql->push_back(eq); - if(Debug.isOn("uf")) { - Debug("uf") << " size is now " << eql->size() << endl; - } -} - -void TheoryUFMorgan::addDisequality(TNode eq) { - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - - TNode a = eq[0]; - TNode b = eq[1]; - - appendToDiseqList(find(a), eq); - appendToDiseqList(find(b), eq); -} - -void TheoryUFMorgan::registerEqualityForPropagation(TNode eq) { - // should NOT be in search at this point, this must be called during - // preregistration - - // FIXME with lemmas on demand, this could miss future propagations, - // since we are not necessarily at context level 0, but are updating - // context-sensitive structures. - - Assert(eq.getKind() == kind::EQUAL || - eq.getKind() == kind::IFF); - - TNode a = eq[0]; - TNode b = eq[1]; - - appendToEqList(find(a), eq); - appendToEqList(find(b), eq); -} - -void TheoryUFMorgan::check(Effort level) { - TimerStat::CodeTimer codeTimer(d_checkTimer); - - Debug("uf") << "uf: begin check(" << level << ")" << endl; - - while(!done()) { - Assert(d_conflict.isNull()); - - Node assertion = get(); - - //d_activeAssertions.push_back(assertion); - - Debug("uf") << "uf check(): " << assertion << endl; - - switch(assertion.getKind()) { - case kind::EQUAL: - case kind::IFF: - d_cc.addEquality(assertion); - if(!d_conflict.isNull()) { - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } - merge(assertion[0], assertion[1]); - break; - case kind::APPLY_UF: - { // predicate - - // assert it's a predicate - Assert(assertion.getOperator().getType().getRangeType().isBoolean()); - - Node eq = NodeManager::currentNM()->mkNode(kind::IFF, - assertion, d_trueNode); - d_cc.addTerm(assertion); - d_cc.addEquality(eq); - - if(!d_conflict.isNull()) { - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } - - if(Debug.isOn("uf")) { - Debug("uf") << "true == false ? " - << (find(d_trueNode) == find(d_falseNode)) << endl; - } - - Assert(find(d_trueNode) != find(d_falseNode)); - - merge(eq[0], eq[1]); - } - break; - case kind::NOT: - if(assertion[0].getKind() == kind::EQUAL || - assertion[0].getKind() == kind::IFF) { - Node a = assertion[0][0]; - Node b = assertion[0][1]; - - addDisequality(assertion[0]); - - d_cc.addTerm(a); - d_cc.addTerm(b); - - if(Debug.isOn("uf")) { - Debug("uf") << " a ==> " << a << endl - << " b ==> " << b << endl - << " find(a) ==> " << debugFind(a) << endl - << " find(b) ==> " << debugFind(b) << endl; - } - - // There are two ways to get a conflict here. - if(!d_conflict.isNull()) { - // We get a conflict this way if we weren't watching a, b - // before and we were just now notified (via - // notifyCongruent()) when we called addTerm() above that - // they are congruent. We make this a separate case (even - // though the check in the "else if.." below would also - // catch it, so that we can clear out d_conflict. - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } else if(find(a) == find(b)) { - // We get a conflict this way if we WERE previously watching - // a, b and were notified previously (via notifyCongruent()) - // that they were congruent. - Node conflict = constructConflict(assertion[0]); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } - - // If we get this far, there should be nothing conflicting due - // to this disequality. - Assert(!d_cc.areCongruent(a, b)); - } else { - // negation of a predicate - Assert(assertion[0].getKind() == kind::APPLY_UF); - - // assert it's a predicate - Assert(assertion[0].getOperator().getType().getRangeType().isBoolean()); - - Node eq = NodeManager::currentNM()->mkNode(kind::IFF, - assertion[0], d_falseNode); - d_cc.addTerm(assertion[0]); - d_cc.addEquality(eq); - - if(!d_conflict.isNull()) { - Node conflict = constructConflict(d_conflict); - d_conflict = Node::null(); - ++d_conflicts; - d_out->conflict(conflict, false); - return; - } - - if(Debug.isOn("uf")) { - Debug("uf") << "true == false ? " - << (find(d_trueNode) == find(d_falseNode)) << endl; - } - - Assert(find(d_trueNode) != find(d_falseNode)); - - merge(eq[0], eq[1]); - } - break; - default: - Unhandled(assertion.getKind()); - } - - /* - if(Debug.isOn("uf")) { - dump(); - } - */ - } - Assert(d_conflict.isNull()); - Debug("uf") << "uf check() done = " << (done() ? "true" : "false") - << endl; - - /* - for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); - diseqIter != d_disequality.end(); - ++diseqIter) { - - TNode left = (*diseqIter)[0]; - TNode right = (*diseqIter)[1]; - if(Debug.isOn("uf")) { - Debug("uf") << "testing left: " << left << endl - << " right: " << right << endl - << " find(L): " << debugFind(left) << endl - << " find(R): " << debugFind(right) << endl - << " areCong: " << d_cc.areCongruent(left, right) - << endl; - } - Assert((debugFind(left) == debugFind(right)) == - d_cc.areCongruent(left, right)); - } - */ - - Debug("uf") << "uf: end check(" << level << ")" << endl; -} - -void TheoryUFMorgan::propagate(Effort level) { - TimerStat::CodeTimer codeTimer(d_propagateTimer); - - Debug("uf") << "uf: begin propagate(" << level << ")" << endl; - // propagation is done in check(), for now - // FIXME need to find a slick way to propagate predicates - Debug("uf") << "uf: end propagate(" << level << ")" << endl; -} - -void TheoryUFMorgan::explain(TNode n) { - TimerStat::CodeTimer codeTimer(d_explainTimer); - - Debug("uf") << "uf: begin explain([" << n << "])" << endl; - Unimplemented(); - Debug("uf") << "uf: end explain([" << n << "])" << endl; -} - -void TheoryUFMorgan::presolve() { - TimerStat::CodeTimer codeTimer(d_presolveTimer); - - Debug("uf") << "uf: begin presolve()" << endl; - if(Options::current()->ufSymmetryBreaker) { - vector<Node> newClauses; - d_symb.apply(newClauses); - for(vector<Node>::const_iterator i = newClauses.begin(); - i != newClauses.end(); - ++i) { - d_out->lemma(*i); - } - } - Debug("uf") << "uf: end presolve()" << endl; -} - -void TheoryUFMorgan::notifyRestart() { - Debug("uf") << "uf: begin notifyDecisionLevelZero()" << endl; - Debug("uf") << "uf: end notifyDecisionLevelZero()" << endl; -} - -Node TheoryUFMorgan::getValue(TNode n) { - NodeManager* nodeManager = NodeManager::currentNM(); - - switch(n.getKind()) { - - case kind::VARIABLE: - case kind::APPLY_UF: - if(n.getType().isBoolean()) { - if(d_cc.areCongruent(d_trueNode, n)) { - return nodeManager->mkConst(true); - } else if(d_cc.areCongruent(d_falseNode, n)) { - return nodeManager->mkConst(false); - } - } - return d_cc.normalize(n); - - case kind::EQUAL: // 2 args - return nodeManager-> - mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); - - default: - Unhandled(n.getKind()); - } -} - -void TheoryUFMorgan::staticLearning(TNode n, NodeBuilder<>& learned) { - TimerStat::CodeTimer codeTimer(d_staticLearningTimer); - - vector<TNode> workList; - workList.push_back(n); - __gnu_cxx::hash_set<TNode, TNodeHashFunction> processed; - - while(!workList.empty()) { - n = workList.back(); - - bool unprocessedChildren = false; - for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - if(processed.find(*i) == processed.end()) { - // unprocessed child - workList.push_back(*i); - unprocessedChildren = true; - } - } - - if(unprocessedChildren) { - continue; - } - - workList.pop_back(); - // has node n been processed in the meantime ? - if(processed.find(n) != processed.end()) { - continue; - } - processed.insert(n); - - // == DIAMONDS == - - Debug("diamonds") << "===================== looking at" << endl - << n << endl; - - // binary OR of binary ANDs of EQUALities - if(n.getKind() == kind::OR && n.getNumChildren() == 2 && - n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 && - n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 && - (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) && - (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) && - (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) && - (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) { - // now we have (a = b && c = d) || (e = f && g = h) - - Debug("diamonds") << "has form of a diamond!" << endl; - - TNode - a = n[0][0][0], b = n[0][0][1], - c = n[0][1][0], d = n[0][1][1], - e = n[1][0][0], f = n[1][0][1], - g = n[1][1][0], h = n[1][1][1]; - - // test that one of {a, b} = one of {c, d}, and make "b" the - // shared node (i.e. put in the form (a = b && b = d)) - // note we don't actually care about the shared ones, so the - // "swaps" below are one-sided, ignoring b and c - if(a == c) { - a = b; - } else if(a == d) { - a = b; - d = c; - } else if(b == c) { - // nothing to do - } else if(b == d) { - d = c; - } else { - // condition not satisfied - Debug("diamonds") << "+ A fails" << endl; - continue; - } - - Debug("diamonds") << "+ A holds" << endl; - - // same: one of {e, f} = one of {g, h}, and make "f" the - // shared node (i.e. put in the form (e = f && f = h)) - if(e == g) { - e = f; - } else if(e == h) { - e = f; - h = g; - } else if(f == g) { - // nothing to do - } else if(f == h) { - h = g; - } else { - // condition not satisfied - Debug("diamonds") << "+ B fails" << endl; - continue; - } - - Debug("diamonds") << "+ B holds" << endl; - - // now we have (a = b && b = d) || (e = f && f = h) - // test that {a, d} == {e, h} - if( (a == e && d == h) || - (a == h && d == e) ) { - // learn: n implies a == d - Debug("diamonds") << "+ C holds" << endl; - Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d); - Debug("diamonds") << " ==> " << newEquality << endl; - learned << n.impNode(newEquality); - } else { - Debug("diamonds") << "+ C fails" << endl; - } - } - } - - if(Options::current()->ufSymmetryBreaker) { - d_symb.assertFormula(n); - } -} - -/* -void TheoryUFMorgan::dump() { - if(!Debug.isOn("uf")) { - return; - } - Debug("uf") << "============== THEORY_UF ==============" << endl; - Debug("uf") << "Active assertions list:" << endl; - for(context::CDList<Node>::const_iterator i = d_activeAssertions.begin(); - i != d_activeAssertions.end(); - ++i) { - Debug("uf") << " " << *i << endl; - } - Debug("uf") << "Congruence union-find:" << endl; - for(UnionFind::const_iterator i = d_unionFind.begin(); - i != d_unionFind.end(); - ++i) { - Debug("uf") << " " << (*i).first << " ==> " << (*i).second - << endl; - } - Debug("uf") << "Disequality lists:" << endl; - for(EqLists::const_iterator i = d_disequalities.begin(); - i != d_disequalities.end(); - ++i) { - Debug("uf") << " " << (*i).first << ":" << endl; - EqList* dl = (*i).second; - for(EqList::const_iterator j = dl->begin(); - j != dl->end(); - ++j) { - Debug("uf") << " " << *j << endl; - } - } - Debug("uf") << "=======================================" << endl; -} -*/ diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h deleted file mode 100644 index e801f383e..000000000 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ /dev/null @@ -1,267 +0,0 @@ -/********************* */ -/*! \file theory_uf_morgan.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of the theory of uninterpreted functions with - ** equality - ** - ** Implementation of the theory of uninterpreted functions with equality, - ** based on CVC4's congruence closure module (which is in turn based on - ** the Nieuwenhuis and Oliveras paper, Fast Congruence Closure and - ** Extensions. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H -#define __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H - -#include "expr/node.h" -#include "expr/attribute.h" - -#include "theory/theory.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/morgan/union_find.h" -#include "theory/uf/symmetry_breaker.h" - -#include "context/context.h" -#include "context/context_mm.h" -#include "context/cdlist.h" -#include "util/congruence_closure.h" - -namespace CVC4 { -namespace theory { -namespace uf { -namespace morgan { - -class TheoryUFMorgan : public TheoryUF { - -private: - - class CongruenceChannel { - TheoryUFMorgan* d_uf; - - public: - CongruenceChannel(TheoryUFMorgan* uf) : d_uf(uf) {} - void notifyCongruent(TNode a, TNode b) { - d_uf->notifyCongruent(a, b); - } - };/* class CongruenceChannel */ - friend class CongruenceChannel; - - /** - * List of all of the non-negated literals from the assertion queue. - * This is used only for conflict generation. - * This differs from pending as the program generates new equalities that - * are not in this list. - * This will probably be phased out in future version. - */ - context::CDList<Node> d_assertions; - - SymmetryBreaker d_symb; - - /** - * Our channel connected to the congruence closure module. - */ - CongruenceChannel d_ccChannel; - - /** - * Instance of the congruence closure module. - */ - CongruenceClosure<CongruenceChannel, CongruenceOperator<kind::APPLY_UF> > d_cc; - - /** - * Our union find for equalities. - */ - UnionFind<TNode, TNodeHashFunction> d_unionFind; - - typedef context::CDList<TNode, context::ContextMemoryAllocator<TNode> > EqList; - typedef context::CDMap<Node, EqList*, NodeHashFunction> EqLists; - - /** List of all disequalities this theory has seen. */ - EqLists d_disequalities; - - /** List of all (potential) equalities to be propagated. */ - EqLists d_equalities; - - Node d_conflict; - - Node d_trueNode, d_falseNode, d_trueEqFalseNode; - - // === STATISTICS === - /** time spent in check() */ - KEEP_STATISTIC(TimerStat, - d_checkTimer, - "theory::uf::morgan::checkTime"); - /** time spent in propagate() */ - KEEP_STATISTIC(TimerStat, - d_propagateTimer, - "theory::uf::morgan::propagateTime"); - - /** time spent in explain() */ - KEEP_STATISTIC(TimerStat, - d_explainTimer, - "theory::uf::morgan::explainTime"); - /** time spent in staticLearning() */ - KEEP_STATISTIC(TimerStat, - d_staticLearningTimer, - "theory::uf::morgan::staticLearningTime"); - /** time spent in presolve() */ - KEEP_STATISTIC(TimerStat, - d_presolveTimer, - "theory::uf::morgan::presolveTime"); - /** number of UF conflicts */ - KEEP_STATISTIC(IntStat, - d_conflicts, - "theory::uf::morgan::conflicts", 0); - /** number of UF propagations */ - KEEP_STATISTIC(IntStat, - d_propagations, - "theory::uf::morgan::propagations", 0); - /** CC module expl length */ - WrappedStat<AverageStat> d_ccExplanationLength; - /** CC module # skolem vars */ - WrappedStat<IntStat> d_ccNewSkolemVars; - -public: - - /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFMorgan(context::Context* ctxt, OutputChannel& out, Valuation valuation); - - /** Destructor for UF theory, cleans up memory and statistics. */ - ~TheoryUFMorgan(); - - /** - * Registers a previously unseen [in this context] node n. - * For TheoryUF, this sets up and maintains invaraints about - * equivalence class data-structures. - * - * Overloads a void registerTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void registerTerm(TNode n); - - /** - * Currently this does nothing. - * - * Overloads a void preRegisterTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void preRegisterTerm(TNode n); - - /** - * Checks whether the set of literals provided to the theory is consistent. - * - * If this is called at any effort level, it computes the congruence closure - * of all of the positive literals in the context. - * - * If this is called at full effort it checks if any of the negative literals - * are inconsistent with the congruence closure. - * - * Overloads void check(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void check(Effort level); - - /** - * Propagates theory literals. - * - * Overloads void propagate(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void propagate(Effort level); - - /** - * Explains a previously theory-propagated literal. - * - * Overloads void explain(TNode n, Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void explain(TNode n); - - /** - * The theory should only add (via .operator<< or .append()) to the - * "learned" builder. It is a conjunction to add to the formula at - * the top-level and may contain other theories' contributions. - */ - void staticLearning(TNode in, NodeBuilder<>& learned); - - /** - * A Theory is called with presolve exactly one time per user - * check-sat. presolve() is called after preregistration, - * rewriting, and Boolean propagation, (other theories' - * propagation?), but the notified Theory has not yet had its - * check() or propagate() method called. A Theory may empty its - * assertFact() queue using get(). A Theory can raise conflicts, - * add lemmas, and propagate literals during presolve(). - */ - void presolve(); - - /** - * Notification sent to the Theory when the search restarts. - */ - void notifyRestart(); - - /** - * Gets a theory value. - * - * Overloads Node getValue(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - Node getValue(TNode n); - - std::string identify() const { return std::string("TheoryUFMorgan"); } - -private: - - /** Constructs a conflict from an inconsistent disequality. */ - Node constructConflict(TNode diseq); - - inline TNode find(TNode a); - inline TNode debugFind(TNode a) const; - - void appendToDiseqList(TNode of, TNode eq); - void appendToEqList(TNode of, TNode eq); - void addDisequality(TNode eq); - void registerEqualityForPropagation(TNode eq); - - /** - * Receives a notification from the congruence closure module that - * two nodes have been merged into the same congruence class. - */ - void notifyCongruent(TNode a, TNode b); - - /** - * Internally handle a congruence, whether generated by the CC - * module or from a theory check(). Merges the classes from a and b - * and looks for a conflict. If there is one, sets d_conflict. - */ - void merge(TNode a, TNode b); - - void dump(); - -};/* class TheoryUFMorgan */ - -inline TNode TheoryUFMorgan::find(TNode a) { - return d_unionFind.find(a); -} - -inline TNode TheoryUFMorgan::debugFind(TNode a) const { - return d_unionFind.debugFind(a); -} - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H */ diff --git a/src/theory/uf/morgan/union_find.cpp b/src/theory/uf/morgan/union_find.cpp deleted file mode 100644 index 135320707..000000000 --- a/src/theory/uf/morgan/union_find.cpp +++ /dev/null @@ -1,61 +0,0 @@ -/********************* */ -/*! \file union_find.cpp - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Path-compressing, backtrackable union-find using an undo - ** stack - ** - ** Path-compressing, backtrackable union-find using an undo stack - ** rather than storing items in a CDMap<>. - **/ - -#include <iostream> - -#include "theory/uf/morgan/union_find.h" -#include "util/Assert.h" -#include "expr/node.h" - -using namespace std; - -namespace CVC4 { -namespace theory { -namespace uf { -namespace morgan { - -template <class NodeType, class NodeHash> -void UnionFind<NodeType, NodeHash>::notify() { - Trace("ufuf") << "UFUF cancelling : " << d_offset << " < " << d_trace.size() << " ?" << endl; - while(d_offset < d_trace.size()) { - pair<TNode, TNode> p = d_trace.back(); - if(p.second.isNull()) { - d_map.erase(p.first); - Trace("ufuf") << "UFUF " << d_trace.size() << " erasing " << p.first << endl; - } else { - d_map[p.first] = p.second; - Trace("ufuf") << "UFUF " << d_trace.size() << " replacing " << p << endl; - } - d_trace.pop_back(); - } - Trace("ufuf") << "UFUF cancelling finished." << endl; -} - -// The following declarations allow us to put functions in the .cpp file -// instead of the header, since we know which instantiations are needed. - -template void UnionFind<Node, NodeHashFunction>::notify(); - -template void UnionFind<TNode, TNodeHashFunction>::notify(); - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ diff --git a/src/theory/uf/morgan/union_find.h b/src/theory/uf/morgan/union_find.h deleted file mode 100644 index 794d7452c..000000000 --- a/src/theory/uf/morgan/union_find.h +++ /dev/null @@ -1,148 +0,0 @@ -/********************* */ -/*! \file union_find.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Path-compressing, backtrackable union-find using an undo - ** stack - ** - ** Path-compressing, backtrackable union-find using an undo stack - ** rather than storing items in a CDMap<>. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__MORGAN__UNION_FIND_H -#define __CVC4__THEORY__UF__MORGAN__UNION_FIND_H - -#include <utility> -#include <vector> -#include <ext/hash_map> - -#include "expr/node.h" -#include "context/cdo.h" - -namespace CVC4 { - -namespace context { - class Context; -}/* CVC4::context namespace */ - -namespace theory { -namespace uf { -namespace morgan { - -// NodeType \in { Node, TNode } -template <class NodeType, class NodeHash> -class UnionFind : context::ContextNotifyObj { - /** Our underlying map type. */ - typedef __gnu_cxx::hash_map<NodeType, NodeType, NodeHash> MapType; - - /** - * Our map of Nodes to their canonical representatives. - * If a Node is not present in the map, it is its own - * representative. - */ - MapType d_map; - - /** Our undo stack for changes made to d_map. */ - std::vector<std::pair<TNode, TNode> > d_trace; - - /** Our current offset in the d_trace stack (context-dependent). */ - context::CDO<size_t> d_offset; - -public: - UnionFind(context::Context* ctxt) : - context::ContextNotifyObj(ctxt), - d_offset(ctxt, 0) { - } - - ~UnionFind() throw() { } - - /** - * Return a Node's union-find representative, doing path compression. - */ - inline TNode find(TNode n); - - /** - * Return a Node's union-find representative, NOT doing path compression. - * This is useful for Assert() statements, debug checking, and similar - * things that you do NOT want to mutate the structure. - */ - inline TNode debugFind(TNode n) const; - - /** - * Set the canonical representative of n to newParent. They should BOTH - * be their own canonical representatives on entry to this funciton. - */ - inline void setCanon(TNode n, TNode newParent); - - /** - * Called by the Context when a pop occurs. Cancels everything to the - * current context level. Overrides ContextNotifyObj::notify(). - */ - void notify(); - -};/* class UnionFind<> */ - -template <class NodeType, class NodeHash> -inline TNode UnionFind<NodeType, NodeHash>::debugFind(TNode n) const { - typename MapType::const_iterator i = d_map.find(n); - if(i == d_map.end()) { - return n; - } else { - return debugFind((*i).second); - } -} - -template <class NodeType, class NodeHash> -inline TNode UnionFind<NodeType, NodeHash>::find(TNode n) { - Trace("ufuf") << "UFUF find of " << n << std::endl; - typename MapType::iterator i = d_map.find(n); - if(i == d_map.end()) { - Trace("ufuf") << "UFUF it is rep" << std::endl; - return n; - } else { - Trace("ufuf") << "UFUF not rep: par is " << (*i).second << std::endl; - std::pair<TNode, TNode> pr = *i; - // our iterator is invalidated by the recursive call to find(), - // since it mutates the map - TNode p = find(pr.second); - if(p == pr.second) { - return p; - } - d_trace.push_back(std::make_pair(n, pr.second)); - d_offset = d_trace.size(); - Trace("ufuf") << "UFUF setting canon of " << n << " : " << p << " @ " << d_trace.size() << std::endl; - pr.second = p; - d_map.insert(pr); - return p; - } -} - -template <class NodeType, class NodeHash> -inline void UnionFind<NodeType, NodeHash>::setCanon(TNode n, TNode newParent) { - Assert(d_map.find(n) == d_map.end()); - Assert(d_map.find(newParent) == d_map.end()); - if(n != newParent) { - Trace("ufuf") << "UFUF setting canon of " << n << " : " << newParent << " @ " << d_trace.size() << std::endl; - d_map[n] = newParent; - d_trace.push_back(std::make_pair(n, TNode::null())); - d_offset = d_trace.size(); - } -} - -}/* CVC4::theory::uf::morgan namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /*__CVC4__THEORY__UF__MORGAN__UNION_FIND_H */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3c8d59d08..401c18203 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -2,10 +2,10 @@ /*! \file theory_uf.cpp ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index de8e70a49..1f4c2372f 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,11 +1,11 @@ /********************* */ /*! \file theory_uf.h ** \verbatim - ** Original author: dejan - ** Major contributors: none + ** Original author: mdeters + ** Major contributors: dejan ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h index ee88df126..e1aba2c95 100644 --- a/src/theory/uf/theory_uf_rewriter.h +++ b/src/theory/uf/theory_uf_rewriter.h @@ -2,7 +2,7 @@ /*! \file theory_uf_rewriter.h ** \verbatim ** Original author: dejan - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h index 7a4bf721f..927a31e01 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -5,7 +5,7 @@ ** Major contributors: cconway, mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/theory/uf/tim/Makefile b/src/theory/uf/tim/Makefile deleted file mode 100644 index e1db2cbf9..000000000 --- a/src/theory/uf/tim/Makefile +++ /dev/null @@ -1,4 +0,0 @@ -topdir = ../../../.. -srcdir = src/theory/uf/tim - -include $(topdir)/Makefile.subdir diff --git a/src/theory/uf/tim/Makefile.am b/src/theory/uf/tim/Makefile.am deleted file mode 100644 index 647783885..000000000 --- a/src/theory/uf/tim/Makefile.am +++ /dev/null @@ -1,14 +0,0 @@ -AM_CPPFLAGS = \ - -D__BUILDING_CVC4LIB \ - -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) - -noinst_LTLIBRARIES = libuftim.la - -libuftim_la_SOURCES = \ - ecdata.h \ - ecdata.cpp \ - theory_uf_tim.h \ - theory_uf_tim.cpp - -EXTRA_DIST = diff --git a/src/theory/uf/tim/ecdata.cpp b/src/theory/uf/tim/ecdata.cpp deleted file mode 100644 index 52a110ff2..000000000 --- a/src/theory/uf/tim/ecdata.cpp +++ /dev/null @@ -1,105 +0,0 @@ -/********************* */ -/*! \file ecdata.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of equivalence class data for UF theory. - ** - ** Implementation of equivalence class data for UF theory. This is a - ** context-dependent object. - **/ - -#include "theory/uf/tim/ecdata.h" - -using namespace CVC4; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; -using namespace CVC4::theory::uf::tim; - -ECData::ECData(Context * context, TNode n) : - ContextObj(context), - d_find(this), - d_rep(n), - d_watchListSize(0), - d_first(NULL), - d_last(NULL) { -} - -bool ECData::isClassRep() { - return this == this->d_find; -} - -void ECData::addPredecessor(TNode n) { - Assert(isClassRep()); - - makeCurrent(); - - Link * newPred = new(getCMM()) Link(getContext(), n, d_first); - d_first = newPred; - if(d_last == NULL) { - d_last = newPred; - } - - ++d_watchListSize; -} - -ContextObj* ECData::save(ContextMemoryManager* pCMM) { - return new(pCMM) ECData(*this); -} - -void ECData::restore(ContextObj* pContextObj) { - ECData* data = (ECData*)pContextObj; - d_find = data->d_find; - d_first = data->d_first; - d_last = data->d_last; - d_rep = data->d_rep; - d_watchListSize = data->d_watchListSize; -} - -Node ECData::getRep() { - return d_rep; -} - -unsigned ECData::getWatchListSize() { - return d_watchListSize; -} - -void ECData::setFind(ECData * ec) { - makeCurrent(); - d_find = ec; -} - -ECData* ECData::getFind() { - return d_find; -} - -Link* ECData::getFirst() { - return d_first; -} - -void ECData::takeOverDescendantWatchList(ECData* nslave, ECData* nmaster) { - Assert(nslave != nmaster); - Assert(nslave->getFind() == nmaster); - - nmaster->makeCurrent(); - - nmaster->d_watchListSize += nslave->d_watchListSize; - - if(nmaster->d_first == NULL) { - nmaster->d_first = nslave->d_first; - nmaster->d_last = nslave->d_last; - } else if(nslave->d_first != NULL) { - Link* currLast = nmaster->d_last; - currLast->d_next = nslave->d_first; - nmaster->d_last = nslave->d_last; - } -} diff --git a/src/theory/uf/tim/ecdata.h b/src/theory/uf/tim/ecdata.h deleted file mode 100644 index 5e72f0042..000000000 --- a/src/theory/uf/tim/ecdata.h +++ /dev/null @@ -1,261 +0,0 @@ -/********************* */ -/*! \file ecdata.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Context dependent equivalence class datastructure for nodes. - ** - ** Context dependent equivalence class datastructure for nodes. - ** Currently keeps a context dependent watch list. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H -#define __CVC4__THEORY__UF__TIM__ECDATA_H - -#include "expr/node.h" -#include "context/context.h" -#include "context/cdo.h" -#include "context/context_mm.h" - -namespace CVC4 { -namespace theory { -namespace uf { -namespace tim { - -/** - * Link is a context dependent linked list of nodes. - * Link is intended to be allocated in a Context's memory manager. - * The next pointer of the list is context dependent, but the node being - * pointed to is fixed for the life of the Link. - * - * Clients of Link are intended not to modify the node that is being pointed - * to in good faith. This may change in the future. - */ -struct Link { - /** - * Pointer to the next element in linked list. - * This is context dependent. - */ - context::CDO<Link*> d_next; - - /** - * Link is supposed to be allocated in a region of a - * ContextMemoryManager. In order to avoid having to decrement the - * ref count at deletion time, it is preferrable for the user of - * Link to maintain the invariant that data will survival for the - * entire scope of the TNode. - */ - TNode d_data; - - /** - * Creates a new Link w.r.t. a context for the node n. - * An optional parameter is to specify the next element in the link. - */ - Link(context::Context* context, TNode n, Link* l = NULL) : - d_next(true, context, l), - d_data(n) { - Debug("context") << "Link: " << this - << " so cdo is " << &d_next << std::endl; - } - - /** - * Allocates a new Link in the region for the provided ContextMemoryManager. - * This allows for cheap cleanup on pop. - */ - static void* operator new(size_t size, context::ContextMemoryManager* pCMM) { - return pCMM->newData(size); - } - -private: - - /** - * The destructor isn't actually defined. This declaration keeps - * the compiler from creating (wastefully) a default definition, and - * ensures that we get a link error if someone uses Link in a way - * that requires destruction. Objects of class Link should always - * be allocated in a ContextMemoryManager, which doesn't call - * destructors. - */ - ~Link() throw(); - - /** - * Just like the destructor, this is not defined. This ensures no - * one tries to create a Link on the heap. - */ - static void* operator new(size_t size); - -};/* struct Link */ - - -/** - * ECData is a equivalence class object that is context dependent. - * It is developed in order to support the congruence closure algorithm - * in TheoryUF, and is not intended to be used outside of that package. - * - * ECData maintains: - * - find pointer for the equivalence class (disjoint set forest) - * - the node that represents the equivalence class. - * - maintains a predecessorlist/watchlist - * - * ECData does not have support for the canonical find and union operators - * for disjoint set forests. Instead it only provides access to the find - * pointer. The implementation of find is ccFind in TheoryUF. - * union is broken into 2 phases: - * 1) setting the find point with setFind - * 2) taking over the watch list of the other node. - * This is a technical requirement for the implementation of TheoryUF. - * (See ccUnion in TheoryUF for more information.) - * - * The intended paradigm for iterating over the watch list of ec is: - * for(Link* i = ec->getFirst(); i != NULL; i = i->next ); - * - * See also ECAttr() in theory_uf.h, and theory_uf.cpp where the codde that uses - * ECData lives. - */ -class ECData : public context::ContextObj { -private: - /** - * This is the standard disjoint set forest find pointer. - * - * Why an ECData pointer instead of a node? - * This was chosen to be a ECData pointer in order to shortcut at least one - * table every time the find pointer is examined. - */ - ECData* d_find; - - /** - * This is pointer back to the node that represents this equivalence class. - * - * The following invariant should be maintained: - * (n.getAttribute(ECAttr()))->rep == n - * i.e. rep is equal to the node that maps to the ECData using ECAttr. - * - * Tricky part: This needs to be a TNode, not a Node. - * Suppose that rep were a hard link. - * When a node n maps to an ECData via the ECAttr() there will be a hard - * link back to n in the ECData. The attribute does not do garbage collection - * until the node gets garbage collected, which does not happen until its - * ref count drops to 0. So because of this cycle neither the node and - * the ECData will never get garbage collected. - * So this needs to be a soft link. - */ - TNode d_rep; - - // Watch list data structures follow - - /** - * Maintains watch list size for more efficient merging. - */ - unsigned d_watchListSize; - - /** - * Pointer to the beginning of the watchlist. - * This value is NULL iff the watch list is empty. - */ - Link* d_first; - - /** - * Pointer to the end of the watch-list. - * This is maintained in order to constant time list merging. - * (This does not give any asymptotic improve as this is currently always - * preceeded by an O(|watchlist|) operation.) - * This value is NULL iff the watch list is empty. - */ - Link* d_last; - - /** Context-dependent operation: save this ECData */ - context::ContextObj* save(context::ContextMemoryManager* pCMM); - - /** Context-dependent operation: restore this ECData */ - void restore(context::ContextObj* pContextObj); - -public: - /** - * Returns true if this ECData object is the current representative of - * the equivalence class. - */ - bool isClassRep(); - - /** - * Adds a node to the watch list of the equivalence class. Does - * context-dependent memory allocation in the Context with which - * this ECData was created. - * - * @param n the node to be added. - * @pre isClassRep() == true - */ - void addPredecessor(TNode n); - - /** - * Creates a EQ with the representative n - * @param context the context to associate with this ecdata. - * This is required as ECData is context dependent - * @param n the node that corresponds to this ECData - */ - ECData(context::Context* context, TNode n); - - /** Destructor for ECDatas */ - ~ECData() { - Debug("ufgc") << "Calling ECData destructor" << std::endl; - destroy(); - } - - /** - * An ECData takes over the watch list of another ECData. - * This is the second step in the union operator for ECData. - * This should be called after nslave->setFind(nmaster); - * After this is done nslave's watch list should never be accessed by - * getLast() or getFirst() - */ - static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster); - - /** - * Returns the representative of this ECData. - */ - Node getRep(); - - /** - * Returns the size of the equivalence class. - */ - unsigned getWatchListSize(); - - /** - * Returns a pointer the first member of the watch list. - */ - Link* getFirst(); - - - /** - * Returns the find pointer of the ECData. - * If isClassRep(), then getFind() == this - */ - ECData* getFind(); - - /** - * Sets the find pointer of the equivalence class to be another ECData object. - * - * @pre isClassRep() == true - * @pre ec->isClassRep() == true - * @post isClassRep() == false - * @post ec->isClassRep() == true - */ - void setFind(ECData * ec); - -};/* class ECData */ - -}/* CVC4::theory::uf::tim namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */ diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp deleted file mode 100644 index ae37dfe99..000000000 --- a/src/theory/uf/tim/theory_uf_tim.cpp +++ /dev/null @@ -1,325 +0,0 @@ -/********************* */ -/*! \file theory_uf_tim.cpp - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Implementation of the theory of uninterpreted functions. - ** - ** Implementation of the theory of uninterpreted functions. - **/ - -#include "theory/uf/tim/theory_uf_tim.h" -#include "theory/uf/tim/ecdata.h" -#include "expr/kind.h" - -using namespace CVC4; -using namespace CVC4::kind; -using namespace CVC4::context; -using namespace CVC4::theory; -using namespace CVC4::theory::uf; -using namespace CVC4::theory::uf::tim; - -TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) : - TheoryUF(c, out, valuation), - d_assertions(c), - d_pending(c), - d_currentPendingIdx(c,0), - d_disequality(c), - d_registered(c) { - Warning() << "NOTE:" << std::endl - << "NOTE: currently the 'Tim' UF solver is broken," << std::endl - << "NOTE: since its registerTerm() function is never" << std::endl - << "NOTE: called." << std::endl - << "NOTE:" << std::endl; -} - -TheoryUFTim::~TheoryUFTim() { -} - -void TheoryUFTim::preRegisterTerm(TNode n) { - Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; - Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; -} - -void TheoryUFTim::registerTerm(TNode n) { - - Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl; - - d_registered.push_back(n); - - ECData* ecN; - - if(n.getAttribute(ECAttr(), ecN)) { - /* registerTerm(n) is only called when a node has not been seen in the - * current context. ECAttr() is not a context-dependent attribute. - * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call, - * then it must be the case that this attribute was created in a previous - * and no longer valid context. Because of this we have to reregister the - * predecessors lists. - * Also we do not have to worry about duplicates because all of the Link* - * setup before are removed when the context n was setup in was popped out - * of. All we are going to do here are sanity checks. - */ - - /* - * Consider the following chain of events: - * 1) registerTerm(n) is called on node n where n : f(m) in context level X, - * 2) A new ECData is created on the heap, ecN, - * 3) n is added to the predessecor list of m in context level X, - * 4) We pop out of X, - * 5) n is removed from the predessecor list of m because this is context - * dependent, the Link* will be destroyed and pointers to the Link - * structs in the ECData objects will be updated. - * 6) registerTerm(n) is called on node n in context level Y, - * 7) If n.hasAttribute(ECAttr(), &ecN), then ecN is still around, - * but the predecessor list is not - * - * The above assumes that the code is working correctly. - */ - Assert(ecN->getFirst() == NULL, - "Equivalence class data exists for the node being registered. " - "Expected getFirst() == NULL. " - "This data is either already in use or was not properly maintained " - "during backtracking"); - /*Assert(ecN->getLast() == NULL, - "Equivalence class data exists for the node being registered. " - "Expected getLast() == NULL. " - "This data is either already in use or was not properly maintained " - "during backtracking.");*/ - Assert(ecN->isClassRep(), - "Equivalence class data exists for the node being registered. " - "Expected isClassRep() to be true. " - "This data is either already in use or was not properly maintained " - "during backtracking"); - Assert(ecN->getWatchListSize() == 0, - "Equivalence class data exists for the node being registered. " - "Expected getWatchListSize() == 0. " - "This data is either already in use or was not properly maintained " - "during backtracking"); - } else { - //The attribute does not exist, so it is created and set - ecN = new (true) ECData(getContext(), n); - n.setAttribute(ECAttr(), ecN); - } - - /* If the node is an APPLY_UF, we need to add it to the predecessor list - * of its children. - */ - if(n.getKind() == APPLY_UF) { - TNode::iterator cIter = n.begin(); - - for(; cIter != n.end(); ++cIter) { - TNode child = *cIter; - - /* Because this can be called after nodes have been merged, we need - * to lookup the representative in the UnionFind datastructure. - */ - ECData* ecChild = ccFind(child.getAttribute(ECAttr())); - - /* Because this can be called after nodes have been merged we may need - * to be merged with other predecessors of the equivalence class. - */ - for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ) { - if(equiv(n, Px->d_data)) { - Node pend = n.eqNode(Px->d_data); - d_pending.push_back(pend); - } - } - - ecChild->addPredecessor(n); - } - } - Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl; - -} - -bool TheoryUFTim::sameCongruenceClass(TNode x, TNode y) { - return - ccFind(x.getAttribute(ECAttr())) == - ccFind(y.getAttribute(ECAttr())); -} - -bool TheoryUFTim::equiv(TNode x, TNode y) { - Assert(x.getKind() == kind::APPLY_UF); - Assert(y.getKind() == kind::APPLY_UF); - - if(x.getNumChildren() != y.getNumChildren()) { - return false; - } - - if(x.getOperator() != y.getOperator()) { - return false; - } - - // intentionally don't look at operator - - TNode::iterator xIter = x.begin(); - TNode::iterator yIter = y.begin(); - - while(xIter != x.end()) { - - if(!sameCongruenceClass(*xIter, *yIter)) { - return false; - } - - ++xIter; - ++yIter; - } - return true; -} - -/* This is a very basic, but *obviously correct* find implementation - * of the classic find algorithm. - * TODO after we have done some more testing: - * 1) Add path compression. This is dependent on changes to ccUnion as - * many better algorithms use eager path compression. - * 2) Elminate recursion. - */ -ECData* TheoryUFTim::ccFind(ECData * x) { - if(x->getFind() == x) { - return x; - } else { - return ccFind(x->getFind()); - } - /* Slightly better Find w/ path compression and no recursion*/ - /* - ECData* start; - ECData* next = x; - while(x != x->getFind()) x=x->getRep(); - while( (start = next) != x) { - next = start->getFind(); - start->setFind(x); - } - return x; - */ -} - -void TheoryUFTim::ccUnion(ECData* ecX, ECData* ecY) { - ECData* nslave; - ECData* nmaster; - - if(ecX->getWatchListSize() <= ecY->getWatchListSize()) { - nslave = ecX; - nmaster = ecY; - } else { - nslave = ecY; - nmaster = ecX; - } - - nslave->setFind(nmaster); - - for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ) { - for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ) { - if(equiv(Px->d_data,Py->d_data)) { - Node pendingEq = (Px->d_data).eqNode(Py->d_data); - d_pending.push_back(pendingEq); - } - } - } - - ECData::takeOverDescendantWatchList(nslave, nmaster); -} - -void TheoryUFTim::merge() { - while(d_currentPendingIdx < d_pending.size() ) { - Node assertion = d_pending[d_currentPendingIdx]; - d_currentPendingIdx = d_currentPendingIdx + 1; - - TNode x = assertion[0]; - TNode y = assertion[1]; - - ECData* tmpX = x.getAttribute(ECAttr()); - ECData* tmpY = y.getAttribute(ECAttr()); - - ECData* ecX = ccFind(tmpX); - ECData* ecY = ccFind(tmpY); - if(ecX == ecY) - continue; - - Debug("uf") << "merging equivalence classes for " << std::endl; - Debug("uf") << "left equivalence class :" << (ecX->getRep()) << std::endl; - Debug("uf") << "right equivalence class :" << (ecY->getRep()) << std::endl; - Debug("uf") << std::endl; - - ccUnion(ecX, ecY); - } -} - -Node TheoryUFTim::constructConflict(TNode diseq) { - Debug("uf") << "uf: begin constructConflict()" << std::endl; - - NodeBuilder<> nb(kind::AND); - nb << diseq; - for(unsigned i = 0; i < d_assertions.size(); ++i) { - nb << d_assertions[i]; - } - - Assert(nb.getNumChildren() > 0); - Node conflict = nb.getNumChildren() == 1 ? nb[0] : nb; - - Debug("uf") << "conflict constructed : " << conflict << std::endl; - - Debug("uf") << "uf: ending constructConflict()" << std::endl; - - return conflict; -} - -void TheoryUFTim::check(Effort level) { - - Debug("uf") << "uf: begin check(" << level << ")" << std::endl; - - while(!done()) { - Node assertion = get(); - Debug("uf") << "TheoryUFTim::check(): " << assertion << std::endl; - - switch(assertion.getKind()) { - case EQUAL: - d_assertions.push_back(assertion); - d_pending.push_back(assertion); - merge(); - break; - case NOT: - Assert(assertion[0].getKind() == EQUAL, - "predicates not supported in this UF implementation"); - d_disequality.push_back(assertion[0]); - break; - case APPLY_UF: - Unhandled("predicates not supported in this UF implementation"); - default: - Unhandled(assertion.getKind()); - } - - Debug("uf") << "TheoryUFTim::check(): done = " << (done() ? "true" : "false") << std::endl; - } - - //Make sure all outstanding merges are completed. - if(d_currentPendingIdx < d_pending.size()) { - merge(); - } - - if(standardEffortOrMore(level)) { - for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); - diseqIter != d_disequality.end(); - ++diseqIter) { - - TNode left = (*diseqIter)[0]; - TNode right = (*diseqIter)[1]; - if(sameCongruenceClass(left, right)) { - Node remakeNeq = (*diseqIter).notNode(); - Node conflict = constructConflict(remakeNeq); - d_out->conflict(conflict, false); - return; - } - } - } - - Debug("uf") << "uf: end check(" << level << ")" << std::endl; -} diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h deleted file mode 100644 index 70c60728f..000000000 --- a/src/theory/uf/tim/theory_uf_tim.h +++ /dev/null @@ -1,225 +0,0 @@ -/********************* */ -/*! \file theory_uf_tim.h - ** \verbatim - ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. - ** - ** This is a basic implementation of the Theory of Uninterpreted Functions - ** with Equality. It is based on the Nelson-Oppen algorithm given in - ** "Fast Decision Procedures Based on Congruence Closure" - ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf) - ** This has been extended to work in a context-dependent way. - ** This interacts heavily with the data-structures given in ecdata.h . - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H -#define __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H - -#include "expr/node.h" -#include "expr/attribute.h" - -#include "theory/theory.h" - -#include "context/context.h" -#include "context/cdo.h" -#include "context/cdlist.h" -#include "theory/uf/theory_uf.h" -#include "theory/uf/tim/ecdata.h" - -namespace CVC4 { -namespace theory { -namespace uf { -namespace tim { - -class TheoryUFTim : public TheoryUF { - -private: - - /** - * List of all of the non-negated literals from the assertion queue. - * This is used only for conflict generation. - * This differs from pending as the program generates new equalities that - * are not in this list. - * This will probably be phased out in future version. - */ - context::CDList<Node> d_assertions; - - /** - * List of pending equivalence class merges. - * - * Tricky part: - * Must keep a hard link because new equality terms are created and appended - * to this list. - */ - context::CDList<Node> d_pending; - - /** Index of the next pending equality to merge. */ - context::CDO<unsigned> d_currentPendingIdx; - - /** List of all disequalities this theory has seen. */ - context::CDList<Node> d_disequality; - - /** - * List of all of the terms that are registered in the current context. - * When registerTerm is called on a term we want to guarentee that there - * is a hard link to the term for the duration of the context in which - * register term is called. - * This invariant is enough for us to use soft links where we want is the - * current implementation as well as making ECAttr() not context dependent. - * Soft links used both in ECData, and Link. - */ - context::CDList<Node> d_registered; - -public: - - /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation); - - /** Destructor for the TheoryUF object. */ - ~TheoryUFTim(); - - /** - * Registers a previously unseen [in this context] node n. - * For TheoryUF, this sets up and maintains invaraints about - * equivalence class data-structures. - * - * Overloads a void registerTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void registerTerm(TNode n); - - /** - * Currently this does nothing. - * - * Overloads a void preRegisterTerm(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - void preRegisterTerm(TNode n); - - /** - * Checks whether the set of literals provided to the theory is consistent. - * - * If this is called at any effort level, it computes the congruence closure - * of all of the positive literals in the context. - * - * If this is called at full effort it checks if any of the negative literals - * are inconsistent with the congruence closure. - * - * Overloads void check(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void check(Effort level); - - void presolve() { - // do nothing - } - - /** - * Propagates theory literals. Currently does nothing. - * - * Overloads void propagate(Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void propagate(Effort level) {} - - /** - * Explains a previously reported conflict. Currently does nothing. - * - * Overloads void explain(TNode n, Effort level); from theory.h. - * See theory/theory.h for more information about this method. - */ - void explain(TNode n) {} - - /** - * Get a theory value. - * - * Overloads Node getValue(TNode n); from theory.h. - * See theory/theory.h for more information about this method. - */ - Node getValue(TNode n) { - Unimplemented("TheoryUFTim doesn't support model generation"); - } - - std::string identify() const { return std::string("TheoryUFTim"); } - -private: - /** - * Checks whether 2 nodes are already in the same equivalence class tree. - * This should only be used internally, and it should only be called when - * the only thing done with the equivalence classes is an equality check. - * - * @returns true iff ccFind(x) == ccFind(y); - */ - bool sameCongruenceClass(TNode x, TNode y); - - /** - * Checks whether Node x and Node y are currently congruent - * using the equivalence class data structures. - * @returns true iff - * |x| = n = |y| and - * x.getOperator() == y.getOperator() and - * forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i]) - */ - bool equiv(TNode x, TNode y); - - /** - * Merges 2 equivalence classes, checks wether any predecessors need to - * be set equal to complete congruence closure. - * The class with the smaller class size will be merged. - * @pre ecX->isClassRep() - * @pre ecY->isClassRep() - */ - void ccUnion(ECData* ecX, ECData* ecY); - - /** - * Returns the representative of the equivalence class. - * May modify the find pointers associated with equivalence classes. - */ - ECData* ccFind(ECData* x); - - /** Performs Congruence Closure to reflect the new additions to d_pending. */ - void merge(); - - /** Constructs a conflict from an inconsistent disequality. */ - Node constructConflict(TNode diseq); - -};/* class TheoryUFTim */ - - -/** - * Cleanup function for ECData. This will be used for called whenever - * a ECAttr is being destructed. - */ -struct ECCleanupStrategy { - static void cleanup(ECData* ec) { - Debug("ufgc") << "cleaning up ECData " << ec << "\n"; - ec->deleteSelf(); - } -};/* struct ECCleanupStrategy */ - -/** Unique name to use for constructing ECAttr. */ -struct ECAttrTag {}; - -/** - * ECAttr is the attribute that maps a node to an equivalence class. - */ -typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr; - -}/* CVC4::theory::uf::tim namespace */ -}/* CVC4::theory::uf namespace */ -}/* CVC4::theory namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 5002c8a59..9375998f9 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -2,8 +2,8 @@ /*! \file valuation.cpp ** \verbatim ** Original author: mdeters - ** Major contributors: none - ** Minor contributors (to current version): none + ** Major contributors: taking + ** Minor contributors (to current version): barrett, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -31,16 +31,12 @@ bool Valuation::isSatLiteral(TNode n) const { return d_engine->getPropEngine()->isSatLiteral(n); } -bool Valuation::hasSatValue(TNode n, bool& value) const { - return d_engine->getPropEngine()->hasValue(n, value); -} - -Node Valuation::getSatValue(TNode n) const{ +Node Valuation::getSatValue(TNode n) const { if(n.getKind() == kind::NOT) { Node atomRes = d_engine->getPropEngine()->getValue(n[0]); - if(atomRes.getKind() == kind::CONST_BOOLEAN){ + if(atomRes.getKind() == kind::CONST_BOOLEAN) { return NodeManager::currentNM()->mkConst(!atomRes.getConst<bool>()); - }else{ + } else { Assert(atomRes.isNull()); return atomRes; } @@ -49,5 +45,9 @@ Node Valuation::getSatValue(TNode n) const{ } } +bool Valuation::hasSatValue(TNode n, bool& value) const { + return d_engine->getPropEngine()->hasValue(n, value); +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 58615f481..f819eff9d 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): taking, barrett, dejan ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -57,7 +57,15 @@ public: Node getSatValue(TNode n) const; /** - * Returns true if the node has a sat value. If yes value is set to it's value. + * Returns true if the node has a current SAT assignment. If yes, the + * argument "value" is set to its value. + * + * This is only permitted if n is a theory atom that has an associated + * SAT literal. + * + * @return true if the literal has a current assignment, and returns the + * value in the "value" argument; otherwise false and the "value" + * argument is unmodified. */ bool hasSatValue(TNode n, bool& value) const; |