00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include "qsolver.hh"
00024 #include "implicative.hh"
00025 #include <iostream>
00026
00027 using namespace std;
00028
00029
00030
00031 int main() {
00032 unsigned long int nodes;
00033 unsigned long int steps;
00034
00035
00036 int sc1[] = {1};
00037 bool q1[] = {QECODE_UNIVERSAL};
00038 Implicative test1(1,q1,sc1);
00039 test1.QIntVar(0,1,3);
00040 IntVarArgs b1(1);
00041 b1[0] = test1.var(0);
00042 branch(test1.space(),b1,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00043 test1.nextScope();
00044 post(test1.space(),test1.var(0) == 1);
00045 test1.makeStructure();
00046 QSolver s1(&test1);
00047 nodes=0;
00048 Strategy ret1=s1.solve(nodes);
00049 cout<<"Problem 1 : result = "<<(ret1.isFalse()?"FALSE":"TRUE")<<", sould be FALSE."<<endl;
00050 cout<<nodes<<" nodes."<<endl;
00051
00052
00053
00054 int sc2[] = {1};
00055 bool q2[] = {QECODE_EXISTENTIAL};
00056 Implicative test2(1,q2,sc2);
00057 test2.QIntVar(0,1,3);
00058
00059 IntVarArgs b2(1);
00060 b2[0] = test2.var(0);
00061 branch(test2.space(),b2,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00062
00063 test2.nextScope();
00064 post(test2.space(),test2.var(0) == 1);
00065 test2.makeStructure();
00066 QSolver s2(&test2);
00067 nodes=0;
00068 Strategy ret2=s2.solve(nodes);
00069 cout<<"Problem 2 : result = "<<(ret2.isFalse()?"FALSE":"TRUE")<<", sould be TRUE."<<endl;
00070 cout<<nodes<<" nodes."<<endl;
00071
00072
00073
00074
00075 int sc3[] = {1};
00076 bool q3[] = {QECODE_UNIVERSAL};
00077 Implicative test3(1,q3,sc3);
00078 test3.QIntVar(0,1,3);
00079 post(test3.space(),test3.var(0) == 1);
00080
00081 IntVarArgs b3(1);
00082 b3[0] = test3.var(0);
00083 branch(test3.space(),b3,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00084
00085 test3.nextScope();
00086 post(test3.space(),test3.var(0) == 2);
00087 test3.makeStructure();;
00088 QSolver s3(&test3);
00089 nodes=0;
00090 steps=0;
00091 Strategy ret3=s3.solve(nodes);
00092 cout<<"Problem 3 : result = "<<(ret3.isFalse()?"FALSE":"TRUE")<<", sould be FALSE."<<endl;
00093 cout<<nodes<<" nodes."<<endl;
00094
00095
00096
00097 int sc4[] = {1};
00098 bool q4[] = {QECODE_EXISTENTIAL};
00099 Implicative test4(1,q4,sc4);
00100 test4.QIntVar(0,1,3);
00101 post(test4.space(),test4.var(0) == 1);
00102
00103 IntVarArgs b4(1);
00104 b4[0] = test4.var(0);
00105 branch(test4.space(),b4,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00106
00107 test4.nextScope();
00108 post(test4.space(),test4.var(0) == 2);
00109 test4.makeStructure();
00110 QSolver s4(&test4);
00111 nodes=0;
00112 Strategy ret4=s4.solve(nodes);
00113 cout<<"Problem 4 : result = "<<(ret4.isFalse()?"FALSE":"TRUE")<<", sould be FALSE."<<endl;
00114 cout<<nodes<<" nodes."<<endl;
00115
00116
00117
00118 int sc5[] = {1,1};
00119 bool q5[] = {QECODE_UNIVERSAL,QECODE_EXISTENTIAL};
00120 Implicative test5(2,q5,sc5);
00121 test5.QIntVar(0,1,3);
00122 test5.QIntVar(1,1,3);
00123 post(test5.space(),test5.var(0) == 1);
00124
00125 IntVarArgs b5(1);
00126 b5[0] = test5.var(0);
00127 branch(test5.space(),b5,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00128
00129 test5.nextScope();
00130 post(test5.space(),test5.var(0) == 2);
00131
00132 IntVarArgs b52(2);
00133 b52[0] = test5.var(0);
00134 b52[1] = test5.var(1);
00135 branch(test5.space(),b52,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00136
00137 test5.nextScope();
00138 post(test5.space(),test5.var(1) == 1);
00139 test5.makeStructure();
00140 QSolver s5(&test5);
00141 nodes=0;
00142 steps=0;
00143 Strategy ret5=s5.solve(nodes);
00144 cout<<"Problem 5 : result = "<<(ret5.isFalse()?"FALSE":"TRUE")<<", sould be FALSE."<<endl;
00145 cout<<nodes<<" nodes."<<endl;
00146
00147
00148
00149 int sc6[] = {1,1};
00150 bool q6[] = {QECODE_UNIVERSAL,QECODE_EXISTENTIAL};
00151 Implicative test6(2,q6,sc6);
00152 test6.QIntVar(0,1,3);
00153 test6.QIntVar(1,1,3);
00154 post(test6.space(),test6.var(0) == 1);
00155
00156 IntVarArgs b6(1);
00157 b6[0] = test6.var(0);
00158 branch(test6.space(),b6,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00159
00160 test6.nextScope();
00161 post(test6.space(),test6.var(0) == 1);
00162
00163 IntVarArgs b62(2);
00164 b62[0] = test6.var(0);
00165 b62[1] = test6.var(1);
00166 branch(test6.space(),b62,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00167
00168 test6.nextScope();
00169 post(test6.space(),test6.var(0) == 2);
00170 test6.makeStructure();
00171 QSolver s6(&test6);
00172 nodes=0;
00173 steps=0;
00174 Strategy ret6=s6.solve(nodes);
00175 cout<<"Problem 6 : result = "<<(ret6.isFalse()?"FALSE":"TRUE")<<", sould be FALSE."<<endl;
00176 cout<<nodes<<" nodes."<<endl;
00177
00178
00179
00180 int sc7[] = {1,1};
00181 bool q7[] = {QECODE_EXISTENTIAL,QECODE_UNIVERSAL};
00182 Implicative test7(2,q7,sc7);
00183 test7.QIntVar(0,1,3);
00184 test7.QIntVar(1,0,3);
00185
00186 IntVarArgs b7(1);
00187 b7[0] = test7.var(0);
00188 branch(test7.space(),b7,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00189
00190 test7.nextScope();
00191 post(test7.space(),test7.var(1) <= 2);
00192
00193 IntVarArgs b72(2);
00194 b72[0] = test7.var(0);
00195 b72[1] = test7.var(1);
00196 branch(test7.space(),b72,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00197
00198 test7.nextScope();
00199 post(test7.space(),test7.var(1) == 0);
00200 test7.makeStructure();
00201 QSolver s7(&test7);
00202 nodes=0;
00203 steps=0;
00204 Strategy ret7=s7.solve(nodes);
00205 cout<<"Problem 7 : result = "<<(ret7.isFalse()?"FALSE":"TRUE")<<", sould be FALSE."<<endl;
00206 cout<<nodes<<" nodes."<<endl;
00207
00208
00209
00210 int sc8[] = {1,1};
00211 bool q8[] = {QECODE_EXISTENTIAL,QECODE_UNIVERSAL};
00212 Implicative test8(2,q8,sc8);
00213 test8.QIntVar(0,1,3);
00214 test8.QIntVar(1,0,3);
00215
00216 IntVarArgs b8(1);
00217 b8[0] = test8.var(0);
00218 branch(test8.space(),b8,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00219
00220 test8.nextScope();
00221 post(test8.space(),test8.var(1) == 0);
00222
00223 IntVarArgs b82(2);
00224 b82[0] = test8.var(0);
00225 b82[1] = test8.var(1);
00226 branch(test8.space(),b82,INT_VAR_SIZE_MIN,INT_VAL_MIN);
00227
00228 test8.nextScope();
00229 post(test8.space(),test8.var(1) == 0);
00230 test8.makeStructure();
00231 QSolver s8(&test8);
00232 nodes=0;
00233 steps=0;
00234 Strategy ret8=s8.solve(nodes);
00235 cout<<"Problem 8 : result = "<<(ret8.isFalse()?"FALSE":"TRUE")<<", sould be TRUE."<<endl;
00236 cout<<nodes<<" nodes."<<endl;
00237
00238 }
00239
00240