CVC3

circuit.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file circuit.cpp
00004  * \brief Circuit class
00005  * 
00006  * <hr>
00007  *
00008  * License to use, copy, modify, sell and/or distribute this software
00009  * and its documentation for any purpose is hereby granted without
00010  * royalty, subject to the terms and conditions defined in the \ref
00011  * LICENSE file provided with this distribution.
00012  * 
00013  * <hr>
00014  * 
00015  */
00016 /*****************************************************************************/
00017 
00018 
00019 #include "circuit.h"
00020 #include "search_fast.h"
00021 #include "search_rules.h"
00022 
00023 using namespace std;
00024 
00025 namespace CVC3
00026 {
00027 
00028 Circuit::Circuit(SearchEngineFast* se, const Theorem& thm)
00029   : d_thm(thm)
00030 {
00031   const Expr& e = d_thm.getExpr();
00032   for (int i = 0; i < e.arity(); i++)
00033   {
00034     d_lits[i] =
00035       e[i].isNot() ?
00036       Literal(Variable(se->d_vm, e[i][0]), false) :
00037       Literal(Variable(se->d_vm, e[i]), true);
00038 
00039     se->d_circuitsByExpr[e[i]].push_back(this);
00040     se->d_circuitsByExpr[e[i].negate()].push_back(this);
00041   }
00042 }
00043 
00044 #define vals3(a, b, c) ((a) + 1 + ((b) + 1) * 3 + ((c) + 1) * 9)
00045 #define vals4(a, b, c, d) (vals3(a, b, c) + ((d) + 1) * 27)
00046 
00047 bool Circuit::propagate(SearchEngineFast* se)
00048 {
00049   int v0 = d_lits[0].getValue();
00050   int v1 = d_lits[1].getValue();
00051   int v2 = d_lits[2].getValue();
00052   int v3 = d_lits[3].getValue();
00053 
00054   const Theorem& t0 = d_lits[0].getTheorem();
00055   const Theorem& t1 = d_lits[1].getTheorem();
00056   const Theorem& t2 = d_lits[2].getTheorem();
00057   const Theorem& t3 = d_lits[3].getTheorem();
00058 
00059   int values = d_thm.getExpr().arity() == 3 ?
00060     vals3(v0, v1, v2) : vals4(v0, v1, v2, v3);
00061 
00062   Theorem thm;
00063   Theorem thm2;
00064 
00065   switch (d_thm.getExpr().getKind())
00066   {
00067   case AND_R:
00068     switch (values)
00069     {
00070     case vals3(0,0,0): case vals3(0,0,1): case vals3(0,1,0):
00071     case vals3(1,1,1): case vals3(-1,0,0): case vals3(-1,0,-1):
00072     case vals3(-1,1,-1): case vals3(-1,-1,0): case vals3(-1,-1,1):
00073     case vals3(-1,-1,-1):
00074       break;
00075 
00076     case vals3(0,0,-1): case vals3(0,1,-1): case vals3(0,-1,0):
00077     case vals3(0,-1,1): case vals3(0,-1,-1):
00078       // simp
00079       thm = se->d_rules->propAndrAF(d_thm, v1 == -1, v1 == -1 ? t1 : t2);
00080       break;
00081 
00082     case vals3(0,1,1):
00083       // simp
00084       thm = se->d_rules->propAndrAT(d_thm, t1, t2);
00085       break;
00086 
00087     case vals3(1,1,0): case vals3(1,0,1): case vals3(1,0,0):
00088       // split cases to avoid doing extra work?
00089       se->d_rules->propAndrLRT(d_thm, t0, &thm, &thm2);
00090       break;
00091 
00092     case vals3(-1,0,1):
00093       thm = se->d_rules->propAndrLF(d_thm, t0, t2);
00094       break;
00095 
00096     case vals3(-1,1,0):
00097       thm = se->d_rules->propAndrRF(d_thm, t0, t1);
00098       break;
00099 
00100     case vals3(1,0,-1): case vals3(1,1,-1): case vals3(1,-1,0):
00101     case vals3(1,-1,1): case vals3(1,-1,-1):
00102       se->d_conflictTheorem =
00103   se->d_rules->confAndrAT(d_thm, t0, v1 == -1, v1 == -1 ? t1 : t2);
00104       return false;
00105 
00106     case vals3(-1,1,1):
00107       se->d_conflictTheorem =
00108   se->d_rules->confAndrAF(d_thm, t0, t1, t2);
00109       return false;
00110     }
00111     break;
00112 
00113   case IFF_R:
00114     switch (values)
00115     {
00116     case vals3(0,0,0): case vals3(0,0,1): case vals3(0,0,-1):
00117     case vals3(0,1,0): case vals3(0,-1,0): case vals3(1,0,0):
00118     case vals3(1,1,1): case vals3(1,-1,-1): case vals3(-1,0,0):
00119     case vals3(-1,1,-1): case vals3(-1,-1,1):
00120       break;
00121 
00122     case vals3(0,1,1): case vals3(0,-1,-1):
00123     case vals3(0,1,-1): case vals3(0,-1,1):
00124       // simp
00125       thm = se->d_rules->propIffr(d_thm, 0, t1, t2);
00126       break;
00127 
00128     case vals3(1,0,1): case vals3(-1,0,-1):
00129     case vals3(1,0,-1): case vals3(-1,0,1):
00130       thm = se->d_rules->propIffr(d_thm, 1, t0, t2);
00131       break;
00132 
00133     case vals3(1,1,0): case vals3(-1,-1,0):
00134     case vals3(1,-1,0): case vals3(-1,1,0):
00135       thm = se->d_rules->propIffr(d_thm, 2, t0, t1);
00136       break;
00137 
00138     case vals3(1,1,-1): case vals3(1,-1,1):
00139     case vals3(-1,1,1): case vals3(-1,-1,-1):
00140       se->d_conflictTheorem = se->d_rules->confIffr(d_thm, t0, t1, t2);
00141       return false;
00142     }
00143     break;
00144 
00145   case ITE_R:
00146     switch (values)
00147     {
00148     case vals4(0,0,0,0): case vals4(0,0,0,1): case vals4(0,0,0,-1):
00149     case vals4(0,0,1,0): case vals4(0,0,1,1): case vals4(0,0,1,-1):
00150     case vals4(0,0,-1,0): case vals4(0,0,-1,1): case vals4(0,0,-1,-1):
00151     case vals4(0,1,0,0): case vals4(0,1,0,1): case vals4(0,1,0,-1):
00152     case vals4(0,-1,0,0): case vals4(0,-1,1,0): case vals4(0,-1,-1,0):
00153     case vals4(1,0,0,0): case vals4(1,0,0,1): case vals4(1,0,1,0):
00154     case vals4(1,0,1,1): case vals4(1,1,1,0): case vals4(1,1,1,1):
00155     case vals4(1,1,1,-1): case vals4(1,-1,0,1): case vals4(1,-1,1,1):
00156     case vals4(1,-1,-1,1): case vals4(-1,0,0,0): case vals4(-1,0,0,-1):
00157     case vals4(-1,0,-1,0): case vals4(-1,0,-1,-1): case vals4(-1,1,-1,0):
00158     case vals4(-1,1,-1,1): case vals4(-1,1,-1,-1): case vals4(-1,-1,0,-1):
00159     case vals4(-1,-1,1,-1): case vals4(-1,-1,-1,-1):
00160       break;
00161 
00162     case vals4(0,1,1,0): case vals4(0,1,1,1): case vals4(0,1,1,-1):
00163     case vals4(0,1,-1,0): case vals4(0,1,-1,1): case vals4(0,1,-1,-1):
00164     case vals4(0,-1,0,-1): case vals4(0,-1,1,-1): case vals4(0,-1,-1,-1):
00165     case vals4(0,-1,0,1): case vals4(0,-1,1,1): case vals4(0,-1,-1,1):
00166       // simp
00167       thm = se->d_rules->propIterIte(d_thm, v1 == 1, t1, v1 == 1 ? t2 : t3);
00168       break;
00169 
00170     case vals4(1,0,0,-1): case vals4(1,0,1,-1): case vals4(1,0,-1,0):
00171     case vals4(1,0,-1,1): case vals4(-1,0,0,1): case vals4(-1,0,1,0):
00172     case vals4(-1,0,1,-1): case vals4(-1,0,-1,1):
00173       se->d_rules->propIterIfThen(d_thm, v0 == -v2, t0, v0 == -v2 ? t2 : t3,
00174           &thm, &thm2);
00175       break;
00176 
00177     case vals4(1,1,0,0): case vals4(1,1,0,1): case vals4(1,1,0,-1):
00178     case vals4(1,-1,0,0): case vals4(1,-1,1,0): case vals4(1,-1,-1,0):
00179     case vals4(-1,1,0,0): case vals4(-1,1,0,1): case vals4(-1,1,0,-1):
00180     case vals4(-1,-1,0,0): case vals4(-1,-1,1,0): case vals4(-1,-1,-1,0):
00181       thm = se->d_rules->propIterThen(d_thm, t0, t1);
00182       break;
00183 
00184     case vals4(1,0,-1,-1): case vals4(-1,0,1,1):
00185     case vals4(-1,1,1,1): case vals4(1,1,-1,-1):
00186       se->d_conflictTheorem =
00187   se->d_rules->confIterThenElse(d_thm, t0, t2, t3);
00188       return false;
00189 
00190     case vals4(1,1,-1,0): case vals4(1,1,-1,1): case vals4(1,-1,0,-1):
00191     case vals4(1,-1,1,-1): case vals4(1,-1,-1,-1): case vals4(-1,1,1,0):
00192     case vals4(-1,1,1,-1): case vals4(-1,-1,0,1): case vals4(-1,-1,1,1):
00193     case vals4(-1,-1,-1,1):
00194       se->d_conflictTheorem =
00195   se->d_rules->confIterIfThen(d_thm, v1 == 1, t0, t1, v1 == 1 ? t2 : t3);
00196       return false;
00197     }
00198     break;
00199 
00200   default:
00201     DebugAssert(false, "unhandled circuit");
00202   }
00203 
00204   if (!thm.isNull() && se->newLiteral(thm.getExpr()).getValue() == 0)
00205   {
00206     se->d_core->addFact(thm);
00207     se->recordFact(thm);
00208     se->d_literals.push_back(se->newLiteral(thm.getExpr()));
00209     se->d_circuitPropCount++;
00210   }
00211 
00212   if (!thm2.isNull() && se->newLiteral(thm2.getExpr()).getValue() == 0)
00213   {
00214     se->d_core->addFact(thm2);
00215     se->recordFact(thm2);
00216     se->d_literals.push_back(se->newLiteral(thm2.getExpr()));
00217     se->d_circuitPropCount++;
00218   }
00219 
00220   return true;
00221 }
00222 
00223 
00224 } // namespace CVC3
00225