z3 - z3py: How to improve the time efficiency of the following code -

-

this simplified code using similar implementation idea z3py code problem trying solve more complex , takes 1 minute run.

the intuition of following code translate array of integers in inputarray array of months defined enumsort, infer model of montharray.

from z3 import * s = solver()  month,(jan,feb,mar,apr,may,jun,jul,aug,sep,oct,nov,dec)=enumsort('month',['jan','feb','mar','apr','may','jun','jul','aug','sep','oct','nov','dec']) montharray = array('montharray',intsort(), month) inputarray = array('inputarray',intsort(),intsort()) temparray = array('temparray',intsort(),intsort())  intarray = [1,3,6,7,8,3,5,6,3,12,11,5,2,5,7,3,7,3,2,7,12,4,5,1,10,9] idx,num in enumerate(intarray):     temparray = store(temparray,idx,num)  s.add(inputarray==temparray)  length = int('length') s.add(length == len(intarray)) = int('i') s.add(forall(i,implies(and(i>=0,i<length),and(     implies(inputarray[i]==1,montharray[i]==jan),     implies(inputarray[i]==2,montharray[i]==feb),     implies(inputarray[i]==3,montharray[i]==mar),     implies(inputarray[i]==4,montharray[i]==apr),     implies(inputarray[i]==5,montharray[i]==may),     implies(inputarray[i]==6,montharray[i]==jun),     implies(inputarray[i]==7,montharray[i]==jul),     implies(inputarray[i]==8,montharray[i]==aug),     implies(inputarray[i]==9,montharray[i]==sep),     implies(inputarray[i]==10,montharray[i]==oct),     implies(inputarray[i]==11,montharray[i]==nov),     implies(inputarray[i]==12,montharray[i]==dec)     ))))  print s.check() print s.model()

could give me suggestions ways improve time efficiency using code example? thanks.

edit: smt language output calling solver.to_smt2()

(set-info :status unknown) (declare-datatypes () ((month (jan ) (feb ) (mar ) (apr ) (may ) (jun ) (jul ) (aug ) (sep ) (oct ) (nov ) (dec )))) (declare-fun inputarray () (array int int)) (declare-fun length () int) (declare-fun montharray () (array int month)) (assert (= (select inputarray 0) 1)) (assert (= (select inputarray 1) 3)) (assert (= (select inputarray 2) 6)) (assert (= (select inputarray 3) 7)) (assert (= (select inputarray 4) 8)) (assert (= (select inputarray 5) 3)) (assert (= (select inputarray 6) 5)) (assert (= (select inputarray 7) 6)) (assert (= (select inputarray 8) 3)) (assert (= (select inputarray 9) 12)) (assert (= (select inputarray 10) 11)) (assert (= (select inputarray 11) 5)) (assert (= (select inputarray 12) 2)) (assert (= (select inputarray 13) 5)) (assert (= (select inputarray 14) 7)) (assert (= (select inputarray 15) 3)) (assert (= (select inputarray 16) 7)) (assert (= (select inputarray 17) 3)) (assert (= (select inputarray 18) 2)) (assert (= (select inputarray 19) 7)) (assert (= (select inputarray 20) 12)) (assert (= (select inputarray 21) 4)) (assert (= (select inputarray 22) 5)) (assert (= (select inputarray 23) 1)) (assert (= (select inputarray 24) 10)) (assert (= (select inputarray 25) 9)) (assert (= length 26)) (assert (forall ((i int) )(let (($x172 (=> (= (select inputarray i) 12) (= (select montharray i) dec)))) (let (($x175 (=> (= (select inputarray i) 11) (= (select montharray i) nov)))) (let (($x178 (=> (= (select inputarray i) 10) (= (select montharray i) oct)))) (let (($x181 (=> (= (select inputarray i) 9) (= (select montharray i) sep)))) (let (($x184 (=> (= (select inputarray i) 8) (= (select montharray i) aug)))) (let (($x187 (=> (= (select inputarray i) 7) (= (select montharray i) jul)))) (let (($x190 (=> (= (select inputarray i) 6) (= (select montharray i) jun)))) (let (($x193 (=> (= (select inputarray i) 5) (= (select montharray i) may)))) (let (($x196 (=> (= (select inputarray i) 4) (= (select montharray i) apr)))) (let (($x199 (=> (= (select inputarray i) 3) (= (select montharray i) mar)))) (let (($x202 (=> (= (select inputarray i) 2) (= (select montharray i) feb)))) (let (($x205 (=> (= (select inputarray i) 1) (= (select montharray i) jan)))) (=> (and (>= 0) (< length)) (and $x205 $x202 $x199 $x196 $x193 $x190 $x187 $x184 $x181 $x178 $x175 $x172))))))))))))))) ) (check-sat)

i find using 'qflia' (quantifier-free linear integer arithmetic) solver, instead of general solver 'solver()', improve efficiency 3x in case.


Comments

Post a Comment

Popular posts from this blog

PHP DOM loadHTML() method unusual warning -

-
i had following code works fine on localhost: $document = new domdocument(); $document->loadhtml($p_result); $form = $document->getelementsbytagname('form')->item(0); // code continues using $form variable after same code updated on outside server, loadhtml() failed , issued warning. warning: domdocument::loadhtml() expects parameter 1 valid path, string given in path/name/to/script.php returned null instead of object code pretty gets fatal error. note contents of $p_result absolutely same on outside server , on localhost. but why displays kind of warning , why not work? doesn't loadhtml() expects argument 1 string in first place? why method expects parameter 1 valid path ? just make clear i'm not calling loadhtmlfile() , i'm calling loadhtml() . thanks. you're affected one of php bugs . issue present in php 5.6.8 , 5.6.9. have affected php version on server, , bug-free version on localhost. the bug forbids null
Read more

python - How to create jsonb index using GIN on SQLAlchemy? -

-
here's current code creating index jsonb. index("mytable_data_idx_id_key", mytable.data['id'].astext, postgresql_using='gin') but got error. sqlalchemy.exc.programmingerror: (psycopg2.programmingerror) data type text has no default operator class access method "gin" hint: must specify operator class index or define default operator class data type. [sql: "create index event_data_idx_id_key on event using gin ((data ->> 'id'))"] is there way create index on sqlalchemy? the postgresql specific sqlalchemy docs @ http://docs.sqlalchemy.org/en/latest/dialects/postgresql.html#operator-classes mention postgresql_ops dictionary provide "operator class" used postgresql, , provide example illustrating use: index('my_index', my_table.c.id, my_table.c.data, postgresql_ops={ 'data': 'text_pattern_ops',
Read more

c# - TransactionScope not rolling back although no complete() is called -

-
i'm using transactionscope rollback transaction fail bool errorreported = false; action<importerrorlog> newerrorcallback = e => { errorreported = true; errorcallback(e); }; using (var transaction = new transactionscope()) { foreach (importtaskdefinition task in taskdefinition) { loader.load(streamfile, newerrorcallback, task.destinationtable, processingtaskid); } if (!errorreported) transaction.complete(); } i'm sure there no transactionscope started ahead or after code. i'm using entity framework insert in db. regardless state of errorreported transaction never rolled in case of error. what missing ? transactionscope sets transaction.current . that's does. wants transacted must @ property. i believe ef each time connection opened reason. probably, connection open when scope installed. open connection inside of scope or enlist manually. ef has nasty "design decision": default opens
Read more